awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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))))))
have a : e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))))) ≫
  e.inverse.map (e.counitIso.hom.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
Tactic: dsimp only [Functor.mapIso_hom, Iso.app_hom]
-- 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.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))))) ≫
    e.inverse.map (e.counitIso.hom.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
have a : e.inverse.map
  (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))) ≫
    e.counitIso.hom.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
Tactic: rw [← map_comp e.inverse]
-- 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.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))) ≫
      e.counitIso.hom.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
have a : e.inverse.map (𝟙 ((e.inverse ⋙ e.functor).obj (e.functor.obj (e.inverse.obj Y))))
Tactic: rw [e.counit_naturality, e.counitIso.hom_inv_id_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.inverse.map (𝟙 ((e.inverse ⋙ e.functor).obj (e.functor.obj (e.inverse.obj Y))))
have a : e.inverse.map (𝟙 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
Tactic: dsimp only [Functor.comp_obj]
-- 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.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
have a : 𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
Tactic: rw [map_id]
-- 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.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))))))
have a : 𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
Tactic: dsimp only [Functor.mapIso_hom, Iso.app_hom]
    rw [← map_comp e.inverse]
    dsimp
    rw [e.counit_naturality, e.counitIso.hom_inv_id_app]
    dsimp only [Functor.comp_obj]
    rw [map_id]
-- 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))))) ≫
          ((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)
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.obj (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 3 4 =>
    dsimp only [Functor.mapIso_hom, Iso.app_hom]
    rw [← map_comp e.inverse]
    dsimp
    rw [e.counit_naturality, e.counitIso.hom_inv_id_app]
    dsimp only [Functor.comp_obj]
    rw [map_id]
-- 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.obj (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)
have rw : e.unit.app (e.inverse.obj Y) ≫
    e.inverse.map (e.functor.map (e.unit.app (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: rw [id_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.inverse.map (e.functor.map (e.unit.app (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))))))
have a : e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
  e.inverse.map (e.counitIso.inv.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
Tactic: dsimp only [Functor.mapIso_inv, 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.functor.map (e.unit.app (e.inverse.obj Y))) ≫
    e.inverse.map (e.counitIso.inv.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
have a : e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
  e.inverse.map (e.functor.map (e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))))
Tactic: rw [← map_comp e.inverse, ← e.counitInv_naturality, 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.inverse.map (e.functor.map (e.unit.app (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))))))
have a : e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
  e.inverse.map (e.functor.map (e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))))
Tactic: dsimp only [Functor.mapIso_inv, Iso.app_inv]
    rw [← map_comp e.inverse, ← e.counitInv_naturality, 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.functor.map (e.unit.app (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)
have slice_lhs : Eq (α := e.inverse.obj Y ⟶ e.inverse.obj Y)
  (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.inverse.map (e.functor.map (e.unit.app (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 ⟶ e.inverse.obj Y)
  (𝟙 (e.inverse.obj Y) : e.inverse.obj Y ⟶ e.inverse.obj Y)
Tactic: slice_lhs 2 3 =>
    dsimp only [Functor.mapIso_inv, Iso.app_inv]
    rw [← map_comp e.inverse, ← e.counitInv_naturality, 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.inverse.map (e.functor.map (e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))))) ≫
    e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
have a : e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
  e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))
Tactic: rw [e.unitInv_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
⊢ Eq (α := e.inverse.obj Y ⟶ e.inverse.obj Y)
    (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.inverse.map (e.functor.map (e.unit.app (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 ⟶ e.inverse.obj Y)
    (𝟙 (e.inverse.obj Y) : e.inverse.obj Y ⟶ e.inverse.obj Y)
have slice_lhs : e.unit.app (e.inverse.obj Y) ≫
    e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
      ((e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
            e.inverse.map (e.functor.map (e.unit.app (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 3 4 => rw [e.unitInv_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.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))
have a : e.inverse.map (e.functor.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (𝟭 C) (e.inverse.obj Y))))
Tactic: rw [← map_comp e.inverse, ← map_comp e.functor, e.unitIso.hom_inv_id_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.inverse.map (e.functor.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (𝟭 C) (e.inverse.obj Y))))
have a : e.inverse.map (e.functor.map (𝟙 (e.inverse.obj Y)))
Tactic: dsimp only [Functor.id_obj]
-- 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.functor.map (𝟙 (e.inverse.obj Y)))
have a : 𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))
Tactic: rw [map_id, map_id]
-- 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.functor.map (e.unit.app (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))
have a : 𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))
Tactic: rw [← map_comp e.inverse, ← map_comp e.functor, e.unitIso.hom_inv_id_app]
    dsimp only [Functor.id_obj]
    rw [map_id, map_id]
-- 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.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
              e.inverse.map (e.functor.map (e.unit.app (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.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
      e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
        𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y) =
  𝟙 (e.inverse.obj Y)
Tactic: slice_lhs 4 5 =>
    rw [← map_comp e.inverse, ← map_comp e.functor, e.unitIso.hom_inv_id_app]
    dsimp only [Functor.id_obj]
    rw [map_id, map_id]
-- 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.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
          𝟙 (e.inverse.obj (e.functor.obj (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.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y) =
  𝟙 (e.inverse.obj Y)
Tactic: rw [id_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.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y)
have a : e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y))) ≫ e.unitInv.app (e.inverse.obj Y)
Tactic: rw [← e.unitInv_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.unitInv.app (e.inverse.obj (e.functor.obj (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.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
      e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y))) ≫ e.unitInv.app (e.inverse.obj Y) =
  𝟙 (e.inverse.obj Y)
Tactic: slice_lhs 3 4 => rw [← e.unitInv_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.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y)))
have a : e.inverse.map (𝟙 ((e.inverse ⋙ e.functor).obj Y))
Tactic: rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_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.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
        e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y))) ≫ e.unitInv.app (e.inverse.obj Y) =
    𝟙 (e.inverse.obj Y)
have slice_lhs : e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (𝟙 ((e.inverse ⋙ e.functor).obj Y)) ≫ e.unitInv.app (e.inverse.obj Y) =
  𝟙 (e.inverse.obj Y)
Tactic: slice_lhs 2 3 =>
    rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)
have dsimp : F.map
      ((((((η.hom.app X ≫ 𝟙 (G.obj (F.obj X))) ≫ G.map (ε.inv.app (F.obj X))) ≫ 𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫
            𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫
          G.map (F.map (η.inv.app X))) ≫
        𝟙 (G.obj (F.obj X))) ≫
    ε.hom.app (F.obj X) =
  𝟙 (F.obj X)
Tactic: dsimp [adjointifyη, Trans.trans]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map
        ((((((η.hom.app X ≫ 𝟙 (G.obj (F.obj X))) ≫ G.map (ε.inv.app (F.obj X))) ≫ 𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫
              𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫
            G.map (F.map (η.inv.app X))) ≫
          𝟙 (G.obj (F.obj X))) ≫
      ε.hom.app (F.obj X) =
    𝟙 (F.obj X)
have simp : F.map (η.hom.app X) ≫ F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) =
  𝟙 (F.obj X)
Tactic: simp only [comp_id, assoc, map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (hypothesis)
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
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) =
    𝟙 (F.obj X)
have this : (G ⋙ F).map (F.map (η.inv.app X)) ≫ ε.hom.app (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X)) =
  ε.hom.app (F.obj ((F ⋙ G).obj X)) ≫ map (𝟭 D) (F.map (η.inv.app X))
Tactic: have := ε.hom.naturality (F.map (η.inv.app X))
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) =
    𝟙 (F.obj X)
have rw : F.map (η.hom.app X) ≫ F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) =
  𝟙 (F.obj X)
Tactic: rw [this]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
have rw : F.map (η.hom.app X) ≫
    (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
  𝟙 (F.obj X)
Tactic: rw [← assoc _ _ (F.map _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (hypothesis)
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
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
have this : Eq (α := (G ⋙ F).obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) (F.obj X)) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) ((G ⋙ F).obj (F.obj X)))
  ((G ⋙ F).map (ε.inv.app (F.obj X)) ≫ ε.hom.app ((G ⋙ F).obj (F.obj X)))
  (ε.hom.app (obj.{v₂, v₂, u₂, u₂} (𝟭 D) (F.obj X)) ≫ map (𝟭 D) (ε.inv.app (F.obj X)))
Tactic: have := ε.hom.naturality (ε.inv.app <| F.obj X)
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  Eq (α := F.obj (G.obj (F.obj X)) ⟶ F.obj (G.obj (F.obj X)))
    (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))))
    (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X))
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
have rw : F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (hypothesis)
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
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
have this : Iso.hom (ε.app (F.obj X)) ≫ Iso.inv (ε.app (F.obj X)) = 𝟙 ((G ⋙ F).obj (F.obj X))
Tactic: have := (ε.app <| F.obj X).hom_inv_id
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
have rw : F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Tactic: rw [this]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
have rw : F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (hypothesis)
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
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
have this : (F.mapIso (η.app X)).hom ≫ (F.mapIso (η.app X)).inv = 𝟙 (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))
Tactic: have := (F.mapIso <| η.app X).hom_inv_id