awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
rw rw₁ : G.obj X = G.obj X
⊢ F.obj X = G.obj X

Tactic:
rw [hX]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
rw rw₁ : G.obj Y = G.obj Y
⊢ G.obj Y = F.obj Y

Tactic:
rw [hY]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
rw rw₁ : G.obj Y = G.obj Y
⊢ F.obj Y = G.obj Y

Tactic:
rw [hY]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
rw rw₁ : G.obj X = G.obj X
⊢ G.obj X = F.obj X

Tactic:
rw [hX]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ F.map e.inv = eqToHom ⋯ ≫ G.map e.inv ≫ eqToHom ⋯

Tactic:
simp only [← IsIso.Iso.inv_hom e, Functor.map_inv, h₂, IsIso.inv_comp, inv_eqToHom,
    Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp, CategoryTheory.Functor.map_inv, CategoryTheory.inv_eqToHom, CategoryTheory.IsIso.Iso.inv_hom
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : F.map f ≍ G.map f
hg : F.map g ≍ G.map g
rw : F.map f ≫ F.map g ≍ G.map f ≫ G.map g
⊢ F.map (f ≫ g) ≍ G.map (f ≫ g)

Tactic:
rw [F.map_comp, G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : F.map f ≍ G.map f
hg : F.map g ≍ G.map g
⊢ F.map f ≫ F.map g ≍ G.map f ≫ G.map g

Tactic:
congr
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
rw rw₁ : G.map (f ≫ g) ≍ G.map (f ≫ g)
⊢ F.map (f ≫ g) ≍ G.map (f ≫ g)

Tactic:
rw [Functor.hext hobj fun _ _ => hmap]

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₃, v₁, u₃, u₁} E C
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
X Y : E
f : X ⟶ Y
⊢ (H ⋙ F).map f ≍ (H ⋙ G).map f

Tactic:
hmap _
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
H : Functor.{v₂, v₃, u₂, u₃} D E
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : F.map f ≍ G.map f
dsimp : H.map (F.map f) ≍ H.map (G.map f)
⊢ (F ⋙ H).map f ≍ (G ⋙ H).map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
H : Functor.{v₂, v₃, u₂, u₃} D E
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : F.map f ≍ G.map f
⊢ H.map (F.map f) ≍ H.map (G.map f)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
H : Functor.{v₂, v₃, u₂, u₃} D E
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
rw rw₁ : (G ⋙ H).map f ≍ (G ⋙ H).map f
⊢ (F ⋙ H).map f ≍ (G ⋙ H).map f

Tactic:
rw [Functor.hext hobj fun _ _ => hmap]

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F = G
X Y : C
f : X ⟶ Y
rw rw₁ : G.map f ≍ G.map f
⊢ F.map f ≍ G.map f

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
p : X = Y
refl : F.map (eqToHom ⋯) = eqToHom ⋯
⊢ F.map (eqToHom p) = eqToHom ⋯

Tactic:
cases p
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ F.map (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
p : X = Y
w : (F.mapIso (eqToIso p)).hom = Iso.hom (eqToIso ⋯)
⊢ F.mapIso (eqToIso p) = eqToIso ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
p : X = Y
w : (F.mapIso (eqToIso ⋯)).hom = Iso.hom (eqToIso ⋯)
⊢ (F.mapIso (eqToIso p)).hom = Iso.hom (eqToIso ⋯)

Tactic:
cases p
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ (F.mapIso (eqToIso ⋯)).hom = Iso.hom (eqToIso ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F = G
X : C
subst : NatTrans.app (eqToHom ⋯) X = eqToHom ⋯
⊢ NatTrans.app (eqToHom h) X = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ NatTrans.app (eqToHom ⋯) X = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
X Y : C
h : X = Y
rw : α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom ⋯)
⊢ α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom ⋯)

Tactic:
rw [α.naturality_assoc]

Premises used: CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom ⋯)

Tactic:
simp [eqToHom_map]

Premises used: CategoryTheory.eqToHom_map
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ f = eqToHom ⋯ ≫ f ≫ eqToHom ⋯

Tactic:
simp only [Category.id_comp, eqToHom_refl, Category.comp_id]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i j : ι
h : i = j
subst : α i = eqToHom ⋯ ≫ α i ≫ eqToHom ⋯
⊢ α i = eqToHom ⋯ ≫ α j ≫ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i : ι
⊢ α i = eqToHom ⋯ ≫ α i ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
β : Sort u_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
C : Type u_2
D : Type u_3
inst_2 : Category.{u_4, u_3} D
F : C → D
X Y : InducedCategory D F
h : X = Y
subst : F X = F X
⊢ F X = F Y

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
β : Sort u_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
C : Type u_2
D : Type u_3
inst_2 : Category.{u_4, u_3} D
F : C → D
X : InducedCategory D F
⊢ F X = F X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_2
D : Type u_3
inst : Category.{u_4, u_3} D
F : C → D
X Y : InducedCategory D F
h : X = Y
subst : Eq.{u_4 + 1} (α := F X ⟶ F X) (Hom.hom (eqToHom ⋯)) (eqToHom ⋯)
⊢ Eq.{u_4 + 1} (α := F X ⟶ F Y) (Hom.hom (eqToHom h)) (eqToHom ⋯)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_2
D : Type u_3
inst : Category.{u_4, u_3} D
F : C → D
X : InducedCategory D F
⊢ Eq.{u_4 + 1} (α := F X ⟶ F X) (Hom.hom (eqToHom ⋯)) (eqToHom ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C : Type u_2
inst_2 : Category.{u_3, u_2} C
P : ObjectProperty.{u_3, u_2} C
X Y : P.FullSubcategory
h : X = Y
subst : X.obj (P := P) = X.obj (P := P)
⊢ X.obj (P := P) = Y.obj (P := P)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C : Type u_2
inst_2 : Category.{u_3, u_2} C
P : ObjectProperty.{u_3, u_2} C
X : P.FullSubcategory
⊢ X.obj (P := P) = X.obj (P := P)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_2
inst : Category.{u_3, u_2} C
P : ObjectProperty.{u_3, u_2} C
X Y : P.FullSubcategory
h : X = Y
subst : InducedCategory.Hom.hom (eqToHom ⋯) = eqToHom ⋯
⊢ InducedCategory.Hom.hom (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u_2
inst : Category.{u_3, u_2} C
P : ObjectProperty.{u_3, u_2} C
X : P.FullSubcategory
⊢ InducedCategory.Hom.hom (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
X Y : D
f : X ⟶ Y
⊢ (e : (a : T) → D) ((e.symm : (a : D) → T) X : T) = X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
X Y : D
f : X ⟶ Y
⊢ Y = (e : (a : T) → D) ((e.symm : (a : D) → T) Y : T)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
x : InducedCategory (C := T) D (⇑e : (a : T) → D)
⊢ Functor.obj.{v₂, v₂, u_2, u_2} (𝟭 (InducedCategory (C := T) D (⇑e : (a : T) → D))) x =
    Functor.obj.{v₂, v₂, u_2, u_2}
      (inducedFunctor (⇑e : (a : T) → D) ⋙
        { obj := (⇑e.symm : (a : D) → T),
          map := fun {X Y : D} (f : X ⟶ Y) ↦ InducedCategory.homMk (eqToHom ⋯ ≫ f ≫ eqToHom ⋯), map_id := ⋯,
          map_comp := ⋯ })
      x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EqToHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
x : D
⊢ Functor.obj.{v₂, v₂, u₂, u₂}
      (Functor.comp.{v₂, v₂, v₂, u₂, u_2, u₂} (D := InducedCategory (C := T) D (⇑e : (a : T) → D))
        { obj := (⇑e.symm : (a : D) → T),
          map := fun {X Y : D} (f : X ⟶ Y) ↦ InducedCategory.homMk (eqToHom ⋯ ≫ f ≫ eqToHom ⋯), map_id := ⋯,
          map_comp := ⋯ }
        (inducedFunctor (⇑e : (a : T) → D)))
      x =
    Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Equivalence.Symmetry
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X Y : Equivalence.{v_1, v_2, u_1, u_2} C D
x : X ⟶ Y
h :
  ∀ (c : C),
    Eq (α :=
      (obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) X).functor.obj c ⟶
        (obj (symmEquivFunctor C D ⋙ symmEquivInverse C D) Y).functor.obj c)
      (NatTrans.app
        (asNatTrans
          (map (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) x ≫
            Iso.hom
              ((fun (e : Equivalence.{v_1, v_2, u_1, u_2} C D) ↦
                  (Iso.refl (obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e) :
                    obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e ≅
                      obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e))
                Y)))
        c)
      (NatTrans.app
        (asNatTrans
          (Iso.hom
              ((fun (e : Equivalence.{v_1, v_2, u_1, u_2} C D) ↦
                  (Iso.refl (obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e) :
                    obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e ≅
                      obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e))
                X) ≫
            map (symmEquivFunctor C D ⋙ symmEquivInverse C D) x))
        c)
⊢ Eq (α := obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) X ⟶ obj (symmEquivFunctor C D ⋙ symmEquivInverse C D) Y)
    (map (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) x ≫
      Iso.hom
        ((fun (e : Equivalence.{v_1, v_2, u_1, u_2} C D) ↦
            (Iso.refl (obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e) :
              obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e ≅ obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e))
          Y))
    (Iso.hom
        ((fun (e : Equivalence.{v_1, v_2, u_1, u_2} C D) ↦
            (Iso.refl (obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e) :
              obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e ≅ obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e))
          X) ≫
      map (symmEquivFunctor C D ⋙ symmEquivInverse C D) x)

Tactic:
ext c
-- Module: Mathlib.CategoryTheory.Equivalence.Symmetry
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X Y : Equivalence.{v_1, v_2, u_1, u_2} C D
x : X ⟶ Y
c : C
⊢ Eq (α :=
    (obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) X).functor.obj c ⟶
      (obj (symmEquivFunctor C D ⋙ symmEquivInverse C D) Y).functor.obj c)
    (NatTrans.app
      (asNatTrans
        (map (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) x ≫
          Iso.hom
            ((fun (e : Equivalence.{v_1, v_2, u_1, u_2} C D) ↦
                (Iso.refl (obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e) :
                  obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e ≅ obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e))
              Y)))
      c)
    (NatTrans.app
      (asNatTrans
        (Iso.hom
            ((fun (e : Equivalence.{v_1, v_2, u_1, u_2} C D) ↦
                (Iso.refl (obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e) :
                  obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e ≅ obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e))
              X) ≫
          map (symmEquivFunctor C D ⋙ symmEquivInverse C D) x))
      c)

Tactic:
simp [symm, symmEquivInverse]

Premises used: CategoryTheory.Equivalence.symmEquivInverse, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Equivalence.Symmetry
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X Y : (Equivalence.{v_2, v_1, u_2, u_1} D C)ᵒᵖ
x : X ⟶ Y
⊢ Eq (α := obj (symmEquivInverse C D ⋙ symmEquivFunctor C D) X ⟶ obj (𝟭 (Equivalence.{v_2, v_1, u_2, u_1} D C)ᵒᵖ) Y)
    (map (symmEquivInverse C D ⋙ symmEquivFunctor C D) x ≫
      Iso.hom
        ((fun (e : (Equivalence.{v_2, v_1, u_2, u_1} D C)ᵒᵖ) ↦
            (Iso.op (Iso.refl (Opposite.unop e)) :
              Opposite.op (obj (symmEquivInverse C D) e).symm ≅ Opposite.op (Opposite.unop e)))
          Y))
    (Iso.hom
        ((fun (e : (Equivalence.{v_2, v_1, u_2, u_1} D C)ᵒᵖ) ↦
            (Iso.op (Iso.refl (Opposite.unop e)) :
              Opposite.op (obj (symmEquivInverse C D) e).symm ≅ Opposite.op (Opposite.unop e)))
          X) ≫
      map (𝟭 (Equivalence.{v_2, v_1, u_2, u_1} D C)ᵒᵖ) x)

Tactic:
simp [symm, symmEquivInverse]

Premises used: CategoryTheory.Equivalence.symmEquivInverse, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Equivalence.Symmetry
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ Eq (α := obj (symmEquivFunctor C D) X ⟶ obj (symmEquivFunctor C D) X)
    (CategoryStruct.comp (Y := obj (symmEquivFunctor C D) (obj (symmEquivInverse C D) (obj (symmEquivFunctor C D) X)))
        (map (symmEquivFunctor C D)
          (NatTrans.app
            (Iso.hom
              (ofComponents
                (fun (e : Equivalence.{v_1, v_2, u_1, u_2} C D) ↦
                  Iso.refl (obj (𝟭 (Equivalence.{v_1, v_2, u_1, u_2} C D)) e))
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom
            (ofComponents (fun (e : (Equivalence.{v_2, v_1, u_2, u_1} D C)ᵒᵖ) ↦ Iso.op (Iso.refl (Opposite.unop e))) ⋯))
          (obj (symmEquivFunctor C D) X)) :
      obj (symmEquivFunctor C D) X ⟶ obj (symmEquivFunctor C D) X)
    (𝟙 (obj (symmEquivFunctor C D) X) : obj (symmEquivFunctor C D) X ⟶ obj (symmEquivFunctor C D) X)

Tactic:
simp [symm, symmEquivInverse]

Premises used: CategoryTheory.Equivalence.symmEquivInverse, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Equivalence.Symmetry
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
X Y Z : (Equivalence.{v_1, v_2, u_1, u_2} C D)ᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
h :
  ∀ (x_2 : Functor.{v_1, v_3, u_1, u_3} C E) (x_3 : D),
    Eq.{v_3 + 1} (α :=
      (obj (functor (Opposite.unop X).congrLeft) x_2).obj x_3 ⟶ (obj (functor (Opposite.unop Z).congrLeft) x_2).obj x_3)
      (NatTrans.app
        (NatTrans.app
          (asNatTrans
            (mkHom
              (map (whiskeringLeft D C E)
                ((conjugateEquiv (Opposite.unop X).toAdjunction (Opposite.unop Z).toAdjunction :
                    (a : (Opposite.unop Z).functor ⟶ (Opposite.unop X).functor) →
                      (Opposite.unop X).inverse ⟶ (Opposite.unop Z).inverse)
                  (asNatTrans (x ≫ x_1).unop)))))
          x_2)
        x_3)
      (NatTrans.app
        (NatTrans.app
          (asNatTrans
            (CategoryStruct.comp (Y := (Opposite.unop Y).congrLeft)
              (mkHom
                (map (whiskeringLeft D C E)
                  ((conjugateEquiv (Opposite.unop X).toAdjunction (Opposite.unop Y).toAdjunction :
                      (a : (Opposite.unop Y).functor ⟶ (Opposite.unop X).functor) →
                        (Opposite.unop X).inverse ⟶ (Opposite.unop Y).inverse)
                    (asNatTrans x.unop))))
              (mkHom
                (map (whiskeringLeft D C E)
                  ((conjugateEquiv (Opposite.unop Y).toAdjunction (Opposite.unop Z).toAdjunction :
                      (a : (Opposite.unop Z).functor ⟶ (Opposite.unop Y).functor) →
                        (Opposite.unop Y).inverse ⟶ (Opposite.unop Z).inverse)
                    (asNatTrans x_1.unop))))))
          x_2)
        x_3)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_1, v_3, u_1, u_3} C E ≌ Functor.{v_2, v_3, u_2, u_3} D E) (Opposite.unop X).congrLeft
      (Opposite.unop Z).congrLeft)
    (mkHom
      (map (whiskeringLeft D C E)
        ((conjugateEquiv (Opposite.unop X).toAdjunction (Opposite.unop Z).toAdjunction :
            (a : (Opposite.unop Z).functor ⟶ (Opposite.unop X).functor) →
              (Opposite.unop X).inverse ⟶ (Opposite.unop Z).inverse)
          (asNatTrans (x ≫ x_1).unop))))
    (CategoryStruct.comp (Y := (Opposite.unop Y).congrLeft)
      (mkHom
        (map (whiskeringLeft D C E)
          ((conjugateEquiv (Opposite.unop X).toAdjunction (Opposite.unop Y).toAdjunction :
              (a : (Opposite.unop Y).functor ⟶ (Opposite.unop X).functor) →
                (Opposite.unop X).inverse ⟶ (Opposite.unop Y).inverse)
            (asNatTrans x.unop))))
      (mkHom
        (map (whiskeringLeft D C E)
          ((conjugateEquiv (Opposite.unop Y).toAdjunction (Opposite.unop Z).toAdjunction :
              (a : (Opposite.unop Z).functor ⟶ (Opposite.unop Y).functor) →
                (Opposite.unop Y).inverse ⟶ (Opposite.unop Z).inverse)
            (asNatTrans x_1.unop)))))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Equivalence.Symmetry
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
X Y Z : (Equivalence.{v_1, v_2, u_1, u_2} C D)ᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
x_2 : Functor.{v_1, v_3, u_1, u_3} C E
x_3 : D
⊢ Eq.{v_3 + 1} (α :=
    (obj (functor (Opposite.unop X).congrLeft) x_2).obj x_3 ⟶ (obj (functor (Opposite.unop Z).congrLeft) x_2).obj x_3)
    (NatTrans.app
      (NatTrans.app
        (asNatTrans
          (mkHom
            (map (whiskeringLeft D C E)
              ((conjugateEquiv (Opposite.unop X).toAdjunction (Opposite.unop Z).toAdjunction :
                  (a : (Opposite.unop Z).functor ⟶ (Opposite.unop X).functor) →
                    (Opposite.unop X).inverse ⟶ (Opposite.unop Z).inverse)
                (asNatTrans (x ≫ x_1).unop)))))
        x_2)
      x_3)
    (NatTrans.app
      (NatTrans.app
        (asNatTrans
          (CategoryStruct.comp (Y := (Opposite.unop Y).congrLeft)
            (mkHom
              (map (whiskeringLeft D C E)
                ((conjugateEquiv (Opposite.unop X).toAdjunction (Opposite.unop Y).toAdjunction :
                    (a : (Opposite.unop Y).functor ⟶ (Opposite.unop X).functor) →
                      (Opposite.unop X).inverse ⟶ (Opposite.unop Y).inverse)
                  (asNatTrans x.unop))))
            (mkHom
              (map (whiskeringLeft D C E)
                ((conjugateEquiv (Opposite.unop Y).toAdjunction (Opposite.unop Z).toAdjunction :
                    (a : (Opposite.unop Z).functor ⟶ (Opposite.unop Y).functor) →
                      (Opposite.unop Y).inverse ⟶ (Opposite.unop Z).inverse)
                  (asNatTrans x_1.unop))))))
        x_2)
      x_3)

Tactic:
simp [← map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X : C
⊢ e.counitIso.inv.app (e.functor.obj X) ≫ e.functor.map (e.unitIso.inv.app X) = 𝟙 (e.functor.obj X)

Tactic:
simpa [functor_unitIso_comp] using Iso.inv_eq_inv
    (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)) (Iso.refl _)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.Iso.trans, CategoryTheory.Equivalence.functor_unitIso_comp, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.counitIso, CategoryTheory.Iso.inv_eq_inv