# This is a combination of 90 commits.

# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# fix all but one decl

# The commit message #12 will be skipped:

# fix last errors

# The commit message #13 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #14 will be skipped:

# Initial file copy from mathport

# The commit message #15 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #19 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# fix some errors

# The commit message #29 will be skipped:

# some more fixes

# The commit message #30 will be skipped:

# more fixes

# The commit message #31 will be skipped:

# finally fixed

# The commit message #32 will be skipped:

# lint

# The commit message #33 will be skipped:

# add porting note for scary warning

# The commit message #34 will be skipped:

# add porting note about proliferation of match

# The commit message #35 will be skipped:

# initial pass

# The commit message #36 will be skipped:

# fix errors

# The commit message #37 will be skipped:

# lint

# The commit message #38 will be skipped:

# fix errors; lint; add porting notes

# The commit message #39 will be skipped:

# fix errors; lint; add porting note

# The commit message #40 will be skipped:

# fix error

# The commit message #41 will be skipped:

# fix some errors

# The commit message #42 will be skipped:

# minor fixes

# The commit message #43 will be skipped:

# fix all but four

# The commit message #44 will be skipped:

# Delete start_port-macos.sh

# The commit message #45 will be skipped:

# fix last errors; lint

# The commit message #46 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #47 will be skipped:

# Initial file copy from mathport

# The commit message #48 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #49 will be skipped:

# get file to build

# The commit message #50 will be skipped:

# lint

# The commit message #51 will be skipped:

# lint some more

# The commit message #52 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #53 will be skipped:

# Initial file copy from mathport

# The commit message #54 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #55 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #56 will be skipped:

# Initial file copy from mathport

# The commit message #57 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #58 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #59 will be skipped:

# Initial file copy from mathport

# The commit message #60 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #61 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #62 will be skipped:

# Initial file copy from mathport

# The commit message #63 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #64 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #65 will be skipped:

# Initial file copy from mathport

# The commit message #66 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #67 will be skipped:

# first pass

# The commit message #68 will be skipped:

# names and removing restate_axiom

# The commit message #69 will be skipped:

# fix lint

# The commit message #70 will be skipped:

# remove spurious edit

# The commit message #71 will be skipped:

# fix errors; lint

# The commit message #72 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #73 will be skipped:

# Initial file copy from mathport

# The commit message #74 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #77 will be skipped:

# push it as far as possible

# The commit message #78 will be skipped:

# minor changes

# The commit message #79 will be skipped:

# seems to work

# The commit message #80 will be skipped:

# add example and equivalence file for testing

# The commit message #81 will be skipped:

# test: create `slice.lean` test file

# The commit message #82 will be skipped:

# remove equivalence.lean

# The commit message #83 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #84 will be skipped:

# add documentation and clean up

# The commit message #85 will be skipped:

# move iteration tactics to core

# The commit message #86 will be skipped:

# add slice to global import file

# The commit message #87 will be skipped:

# modify documentation lines

# The commit message #88 will be skipped:

# add module documentation(?)

# The commit message #89 will be skipped:

# fix module docs

# The commit message #90 will be skipped:

# fix test/slice.lean

Mathlib.lean

@@ -223,12 +223,6 @@ import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.CategoryTheory.Adjunction.Basic
-import Mathlib.CategoryTheory.Adjunction.FullyFaithful
-import Mathlib.CategoryTheory.Adjunction.Mates
-import Mathlib.CategoryTheory.Adjunction.Reflective
-import Mathlib.CategoryTheory.Adjunction.Whiskering
-import Mathlib.CategoryTheory.Arrow
-import Mathlib.CategoryTheory.Balanced
 import Mathlib.CategoryTheory.Bicategory.Basic
 import Mathlib.CategoryTheory.Bicategory.End
 import Mathlib.CategoryTheory.Bicategory.Strict
@@ -238,16 +232,9 @@ import Mathlib.CategoryTheory.Category.GaloisConnection
 import Mathlib.CategoryTheory.Category.KleisliCat
 import Mathlib.CategoryTheory.Category.Preorder
 import Mathlib.CategoryTheory.Category.RelCat
-import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.CategoryTheory.CommSq
 import Mathlib.CategoryTheory.Comma
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
-import Mathlib.CategoryTheory.Conj
-import Mathlib.CategoryTheory.Core
-import Mathlib.CategoryTheory.DiscreteCategory
-import Mathlib.CategoryTheory.Endomorphism
-import Mathlib.CategoryTheory.EpiMono
-import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Equivalence
 import Mathlib.CategoryTheory.EssentialImage
 import Mathlib.CategoryTheory.EssentiallySmall
@@ -263,26 +250,14 @@ import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.InvIsos
-import Mathlib.CategoryTheory.Functor.ReflectsIso
+import Mathlib.CategoryTheory.Functor.ReflectsIsomorphisms
 import Mathlib.CategoryTheory.Groupoid
-import Mathlib.CategoryTheory.Groupoid.Basic
 import Mathlib.CategoryTheory.Iso
-import Mathlib.CategoryTheory.IsomorphismClasses
-import Mathlib.CategoryTheory.LiftingProperties.Adjunction
 import Mathlib.CategoryTheory.LiftingProperties.Basic
-import Mathlib.CategoryTheory.Limits.Cones
-import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
-import Mathlib.CategoryTheory.Monoidal.Category
-import Mathlib.CategoryTheory.Monoidal.Functor
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Opposites
-import Mathlib.CategoryTheory.PEmpty
-import Mathlib.CategoryTheory.PUnit
 import Mathlib.CategoryTheory.Pi.Basic
-import Mathlib.CategoryTheory.Products.Associator
-import Mathlib.CategoryTheory.Products.Basic
-import Mathlib.CategoryTheory.Products.Bifunctor
 import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.Sums.Basic

Mathlib/CategoryTheory/CommSq.lean

@@ -121,7 +121,7 @@ structure LiftStruct (sq : CommSq f i p g) where
 
 namespace LiftStruct
 
-/-- A `LiftStruct` for a commutative square gives a `LiftStruct` for the
+/-- A `lift_struct` for a commutative square gives a `lift_struct` for the
 corresponding square in the opposite category. -/
 @[simps]
 def op {sq : CommSq f i p g} (l : LiftStruct sq) : LiftStruct sq.op
@@ -131,8 +131,8 @@ def op {sq : CommSq f i p g} (l : LiftStruct sq) : LiftStruct sq.op
   fac_right := by rw [← op_comp, l.fac_left]
 #align category_theory.comm_sq.lift_struct.op CategoryTheory.CommSq.LiftStruct.op
 
-/-- A `LiftStruct` for a commutative square in the opposite category
-gives a `LiftStruct` for the corresponding square in the original category. -/
+/-- A `lift_struct` for a commutative square in the opposite category
+gives a `lift_struct` for the corresponding square in the original category. -/
 @[simps]
 def unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} {sq : CommSq f i p g}
     (l : LiftStruct sq) : LiftStruct sq.unop
@@ -142,7 +142,7 @@ def unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B 
   fac_right := by rw [← unop_comp, l.fac_left]
 #align category_theory.comm_sq.lift_struct.unop CategoryTheory.CommSq.LiftStruct.unop
 
-/-- Equivalences of `LiftStruct` for a square and the corresponding square
+/-- Equivalences of `lift_struct` for a square and the corresponding square
 in the opposite category. -/
 @[simps]
 def opEquiv (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.op
@@ -153,7 +153,7 @@ def opEquiv (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.op
   right_inv := by aesop_cat
 #align category_theory.comm_sq.lift_struct.op_equiv CategoryTheory.CommSq.LiftStruct.opEquiv
 
-/-- Equivalences of `LiftStruct` for a square in the oppositive category and
+/-- Equivalences of `lift_struct` for a square in the oppositive category and
 the corresponding square in the original category. -/
 def unopEquiv {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
     (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.unop
@@ -171,7 +171,8 @@ instance subsingleton_liftStruct_of_epi (sq : CommSq f i p g) [Epi i] :
   ⟨fun l₁ l₂ => by
     ext
     rw [← cancel_epi i]
-    simp only [LiftStruct.fac_left]⟩
+    simp only [LiftStruct.fac_left]
+    ⟩
 #align category_theory.comm_sq.subsingleton_lift_struct_of_epi CategoryTheory.CommSq.subsingleton_liftStruct_of_epi
 
 instance subsingleton_liftStruct_of_mono (sq : CommSq f i p g) [Mono p] :
@@ -185,9 +186,9 @@ instance subsingleton_liftStruct_of_mono (sq : CommSq f i p g) [Mono p] :
 variable (sq : CommSq f i p g)
 
 
-/-- The assertion that a square has a `LiftStruct`. -/
+/-- The assertion that a square has a `lift_struct`. -/
 class HasLift : Prop where
-  /-- Square has a `LiftStruct`. -/
+  /-- Square has a `lift_struct`. -/
   exists_lift : Nonempty sq.LiftStruct
 #align category_theory.comm_sq.has_lift CategoryTheory.CommSq.HasLift
 
@@ -219,7 +220,7 @@ theorem iff_unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {
 
 end HasLift
 
-/-- A choice of a diagonal morphism that is part of a `LiftStruct` when
+/-- A choice of a diagonal morphism that is part of a `lift_struct` when
 the square has a lift. -/
 noncomputable def lift [hsq : HasLift sq] : B ⟶ X :=
   hsq.exists_lift.some.l

Mathlib/CategoryTheory/DiscreteCategory.lean

@@ -44,7 +44,7 @@ universe v₁ v₂ v₃ u₁ u₁' u₂ u₃
 
 -- This is intentionally a structure rather than a type synonym
 -- to enforce using `DiscreteEquiv` (or `Discrete.mk` and `Discrete.as`) to move between
--- `Discrete α` and `α`. Otherwise there is too much API leakage.
+-- `discrete α` and `α`. Otherwise there is too much API leakage.
 /-- A wrapper for promoting any type to a category,
 with the only morphisms being equalities.
 -/
@@ -64,7 +64,8 @@ theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X
 
 /-- `Discrete α` is equivalent to the original type `α`.-/
 @[simps]
-def discreteEquiv {α : Type u₁} : Discrete α ≃ α where
+def discreteEquiv {α : Type u₁} : Discrete α ≃ α
+    where
   toFun := Discrete.as
   invFun := Discrete.mk
   left_inv := by aesop_cat
@@ -81,7 +82,8 @@ somewhat annoyingly we have to define `X ⟶ Y` as `ULift (PLift (X = Y))`.
 
 See <https://stacks.math.columbia.edu/tag/001A>
 -/
-instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α) where
+instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α)
+    where
   Hom X Y := ULift (PLift (X.as = Y.as))
   id X := ULift.up (PLift.up rfl)
   comp {X Y Z} g f := by
@@ -105,15 +107,22 @@ instance [Subsingleton α] : Subsingleton (Discrete α) :=
     ext
     apply Subsingleton.elim⟩
 
-/-
-Porting note: It seems that `aesop` currently has no way to add lemmas locally.
+/- ./././Mathport/Syntax/Translate/Expr.lean:334:4: warning: unsupported (TODO): `[tacs] -/
+/-- A simple tactic to run `cases` on any `discrete α` hypotheses. -/
+--unsafe def _root_.tactic.discrete_cases : tactic Unit :=
+--  sorry
+--#align tactic.discrete_cases tactic.discrete_cases
 
-attribute [local tidy] tactic.discrete_cases
-`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), PLift _]]
--/
 
+--run_cmd
+--  add_interactive [`` tactic.discrete_cases]
+
+--attribute [local tidy] tactic.discrete_cases
+--`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), plift _]]
+
+--macro (name := discrete_cases) "discrete_cases" : tactic =>
+--  `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
 /- Porting note: rewrote `discrete_cases` tactic -/
-/-- A simple tactic to run `cases` on any `discrete α` hypotheses. -/
 macro "discrete_cases": tactic =>
   `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
 
@@ -143,7 +152,7 @@ protected abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y :=
       exact h)
 #align category_theory.discrete.eq_to_iso CategoryTheory.Discrete.eqToIso
 
-/-- A variant of `eqToHom` that lifts terms to the discrete category. -/
+/-- A variant of `eq_to_hom` that lifts terms to the discrete category. -/
 abbrev eqToHom' {a b : α} (h : a = b) : Discrete.mk a ⟶ Discrete.mk b :=
   Discrete.eqToHom h
 #align category_theory.discrete.eq_to_hom' CategoryTheory.Discrete.eqToHom'
@@ -163,8 +172,12 @@ variable {C : Type u₂} [Category.{v₂} C]
 instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f :=
   ⟨⟨Discrete.eqToHom (eq_of_hom f).symm, by aesop_cat⟩⟩
 
-/-- Any function `I → C` gives a functor `Discrete I ⥤ C`.-/
-def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C where
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
+/-- Any function `I → C` gives a functor `Discrete I ⥤ C`.
+-/
+def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C
+    where
   obj := F ∘ Discrete.as
   map {X Y} f := by
     dsimp
@@ -195,6 +208,8 @@ def functorComp {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) :
   NatIso.ofComponents (fun X => Iso.refl _) (by aesop_cat)
 #align category_theory.discrete.functor_comp CategoryTheory.Discrete.functorComp
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
 /-- For functors out of a discrete category,
 a natural transformation is just a collection of maps,
 as the naturality squares are trivial.
@@ -203,20 +218,24 @@ as the naturality squares are trivial.
 def natTrans {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ⟶ G.obj i) : F ⟶ G
     where
   app := f
-  naturality := fun {X Y} ⟨⟨g⟩⟩ => by
+  naturality {X Y} g := by
+    rcases g with ⟨⟨g⟩⟩
     discrete_cases
     rcases g
     change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
     simp
 #align category_theory.discrete.nat_trans CategoryTheory.Discrete.natTrans
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
 /-- For functors out of a discrete category,
 a natural isomorphism is just a collection of isomorphisms,
 as the naturality squares are trivial.
 -/
 @[simps!]
 def natIso {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) : F ≅ G :=
-  NatIso.ofComponents f fun ⟨⟨g⟩⟩ => by
+  NatIso.ofComponents f fun g => by
+    rcases g with ⟨⟨g⟩⟩
     discrete_cases
     rcases g
     change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
@@ -228,6 +247,8 @@ theorem natIso_app {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discret
     (i : Discrete I) : (Discrete.natIso f).app i = f i := by aesop_cat
 #align category_theory.discrete.nat_iso_app CategoryTheory.Discrete.natIso_app
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
 /-- Every functor `F` from a discrete category is naturally isomorphic (actually, equal) to
   `discrete.functor (F.obj)`. -/
 @[simp]
@@ -242,11 +263,16 @@ def compNatIsoDiscrete {I : Type u₁} {D : Type u₃} [Category.{v₃} D] (F :
   natIso fun _ => Iso.refl _
 #align category_theory.discrete.comp_nat_iso_discrete CategoryTheory.Discrete.compNatIsoDiscrete
 
-/-- We can promote a type-level `Equiv` to
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
+/-- We can promote a type-level `equiv` to
 an equivalence between the corresponding `discrete` categories.
 -/
 @[simps]
-def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J where
+def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J
+    where
   functor := Discrete.functor (Discrete.mk ∘ (e : I → J))
   inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I))
   unitIso :=
@@ -263,9 +289,10 @@ def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ D
           simp)
 #align category_theory.discrete.equivalence CategoryTheory.Discrete.equivalence
 
-/-- We can convert an equivalence of `discrete` categories to a type-level `Equiv`. -/
+/-- We can convert an equivalence of `discrete` categories to a type-level `equiv`. -/
 @[simps]
-def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β where
+def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β
+    where
   toFun := Discrete.as ∘ h.functor.obj ∘ Discrete.mk
   invFun := Discrete.as ∘ h.inverse.obj ∘ Discrete.mk
   left_inv a := by simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2
@@ -280,23 +307,27 @@ variable {J : Type v₁}
 
 open Opposite
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:18: unsupported
+\  non-interactive tactic tactic.op_induction' -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
 /-- A discrete category is equivalent to its opposite category. -/
 @[simps! functor_obj_as inverse_obj]
 protected def opposite (α : Type u₁) : (Discrete α)ᵒᵖ ≌ Discrete α :=
   let F : Discrete α ⥤ (Discrete α)ᵒᵖ := Discrete.functor fun x => op (Discrete.mk x)
   Equivalence.mk F.leftOp F
-  (NatIso.ofComponents (fun ⟨X⟩ => Iso.refl _) <| fun {X Y} ⟨⟨f⟩⟩ => by
+  (NatIso.ofComponents (fun ⟨X⟩ => Iso.refl _)
+    <| fun {X Y} f => by
       induction X using Opposite.rec
       induction Y using Opposite.rec
+      rcases f with ⟨⟨f⟩⟩
       discrete_cases
       rcases f
       aesop_cat)
   (Discrete.natIso <| fun ⟨X⟩ => Iso.refl _)
-
 /-
-  Porting note:
-  The following is what was generated by mathport:
-
   refine'
     Equivalence.mk (F.leftOp) F _
       (Discrete.natIso fun X =>
@@ -330,3 +361,4 @@ theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F
 end Discrete
 
 end CategoryTheory
+