awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
rw : F.map f ≫ e.hom.app Y = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₁ : e.hom.app X ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₂ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₃ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
rw₄ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ (G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have rw₅ : eqToHom sorry ≫ G.map f = eqToHom sorry ≫ G.map f ≫ eqToHom sorry ≫ eqToHom sorry
Tactic: rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
    Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
rw : F.map f ≫ e.hom.app Y = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₁ : e.hom.app X ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₂ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₃ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
rw₄ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ (G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
rw₅ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯ ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have rw₆ : eqToHom sorry ≫ G.map f = eqToHom sorry ≫ G.map f ≫ eqToHom sorry
Tactic: rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
    Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
rw : F.map f ≫ e.hom.app Y = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₁ : e.hom.app X ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₂ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₃ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
rw₄ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ (G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
rw₅ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯ ≫ eqToHom ⋯
rw₆ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have rw₇ : eqToHom sorry ≫ G.map f = eqToHom sorry ≫ G.map f ≫ 𝟙 (G.obj Y)
Tactic: rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
    Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
rw : F.map f ≫ e.hom.app Y = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₁ : e.hom.app X ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₂ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
rw₃ : eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
rw₄ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ (G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
rw₅ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯ ≫ eqToHom ⋯
rw₆ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
rw₇ : eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ 𝟙 (G.obj Y)
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have rw₈ : eqToHom sorry ≫ G.map f = eqToHom sorry ≫ G.map f
Tactic: rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
    Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.obj X = G.obj X
have rw : G.obj X = G.obj X
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have subst : F.map f = eqToHom sorry ≫ F.map f ≫ eqToHom sorry
Tactic: subst h
Cleared hypotheses: G, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.obj X = G.obj X
have rw : G.obj X = G.obj X
Tactic: rw [hX]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ G.obj Y = F.obj Y
have rw : G.obj Y = G.obj Y
Tactic: rw [hY]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 ⋯
⊢ F.obj Y = G.obj Y
have rw : G.obj Y = G.obj Y
Tactic: rw [hY]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 ⋯
⊢ G.obj X = F.obj X
have rw : G.obj X = G.obj X
Tactic: rw [hX]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 ≫ g) ≍ G.map (f ≫ g)
have rw : F.map f ≫ F.map g ≍ G.map f ≫ G.map g
Tactic: rw [F.map_comp, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.map (f ≫ g) ≍ G.map (f ≫ g)
have rw : G.map (f ≫ g) ≍ G.map (f ≫ g)
Tactic: rw [Functor.hext hobj fun _ _ => hmap]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ (F ⋙ H).map f ≍ (G ⋙ H).map f
have dsimp : H.map (F.map f) ≍ H.map (G.map f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ (F ⋙ H).map f ≍ (G ⋙ H).map f
have rw : (G ⋙ H).map f ≍ (G ⋙ H).map f
Tactic: rw [Functor.hext hobj fun _ _ => hmap]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.map f ≍ G.map f
have rw : G.map f ≍ G.map f
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.map (eqToHom p) = eqToHom ⋯
have refl : F.map (eqToHom sorry) = eqToHom sorry
Tactic: cases p
Cleared hypotheses: Y, p
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F.mapIso (eqToIso p) = eqToIso ⋯
have w : (F.mapIso (eqToIso p)).hom = Iso.hom (eqToIso sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ (F.mapIso (eqToIso p)).hom = Iso.hom (eqToIso ⋯)
have w : (F.mapIso (eqToIso sorry)).hom = Iso.hom (eqToIso sorry)
Tactic: cases p
Cleared hypotheses: Y, p
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ NatTrans.app (eqToHom h) X = eqToHom ⋯
have subst : NatTrans.app (eqToHom sorry) X = eqToHom sorry
Tactic: subst h
Cleared hypotheses: G, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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 = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom ⋯)
have rw : α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom sorry)
Tactic: rw [α.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ α i = eqToHom ⋯ ≫ α j ≫ eqToHom ⋯
have subst : α i = eqToHom sorry ≫ α i ≫ eqToHom sorry
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ F X = F Y
have subst : F X = F X
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ Eq.{u_4 + 1} (α := F X ⟶ F Y) (Hom.hom (eqToHom h)) (eqToHom ⋯)
have subst : Eq.{u_4 + 1} (α := F X ⟶ F X) (Hom.hom (eqToHom sorry)) (eqToHom sorry)
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ X.obj (P := P) = Y.obj (P := P)
have subst : X.obj (P := P) = X.obj (P := P)
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.EqToHom (goal)
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
⊢ InducedCategory.Hom.hom (eqToHom h) = eqToHom ⋯
have subst : InducedCategory.Hom.hom (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence.Symmetry (goal)
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
⊢ 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)
have 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)
Tactic: ext c
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence.Symmetry (goal)
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
⊢ 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)))))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
have rw : e.unit.app (e.inverse.obj Y) ≫
    (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
        e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
      e.inverse.map (e.counit.app Y) =
  𝟙 (e.inverse.obj Y)
Tactic: rw [← id_comp (e.inverse.map _), ← map_id e.inverse, ← counitInv_functor_comp, map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
          e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
have rw : e.unit.app (e.inverse.obj Y) ≫
    (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
        e.unitIso.hom.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
          e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
            e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
      e.inverse.map (e.counit.app Y) =
  𝟙 (e.inverse.obj Y)
Tactic: rw [← Iso.hom_inv_id_assoc (e.unitIso.app _) (e.inverse.map (e.functor.map _)), Iso.app_hom,
    Iso.app_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
    e.unitIso.hom.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
have a : e.unit.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
  e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))
Tactic: rw [← e.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
          e.unitIso.hom.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
            e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
              e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
have slice_lhs : e.unit.app (e.inverse.obj Y) ≫
    (((e.unit.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
            e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))) ≫
          e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
        e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
      e.inverse.map (e.counit.app Y) =
  𝟙 (e.inverse.obj Y)
Tactic: slice_lhs 2 3 => rw [← e.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
Y : D
| e.unit.app (e.inverse.obj Y) ≫ e.unit.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))
have a : e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))
Tactic: rw [← e.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      (((e.unit.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
              e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))) ≫
            e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
          e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
have slice_lhs : ((((e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))) ≫
          e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))) ≫
        e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
      e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
    e.inverse.map (e.counit.app Y) =
  𝟙 (e.inverse.obj Y)
Tactic: slice_lhs 1 2 => rw [← e.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
Y : D
| e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
have a : Iso.hom (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
  Iso.inv (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
    e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
Tactic: rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
Y : D
⊢ ((((e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))) ≫
            e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))) ≫
          e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
        e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
      e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
have slice_lhs : e.unit.app (e.inverse.obj Y) ≫
    e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
      e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))))) ≫
        ((Iso.hom
                (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
              Iso.inv
                  (e.inverse.mapIso
                    (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
                e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
            e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
          e.inverse.map (e.counit.app Y) =
  𝟙 (e.inverse.obj Y)
Tactic: slice_lhs 4 4 =>
    rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]