awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
Y : D
dsimp :
  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)
⊢ 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:
dsimp only [comp_obj, id_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.id_obj
-- 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
Y : D
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)
⊢ 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:
rw [id_comp]

Premises used: CategoryTheory.Category.id_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
Y : D
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)))))
| 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))))))

Tactic:
dsimp only [Functor.mapIso_inv, Iso.app_inv]

Premises used: CategoryTheory.Iso.app_inv, CategoryTheory.Functor.mapIso_inv
-- 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
Y : D
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)))))
| 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:
rw [← map_comp e.inverse, ← e.counitInv_naturality, map_comp]

Premises used: CategoryTheory.Equivalence.counitInv_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.inverse
-- 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
Y : D
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)))))
| 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))))))

Tactic:
dsimp only [Functor.mapIso_inv, Iso.app_inv]
    rw [← map_comp e.inverse, ← e.counitInv_naturality, map_comp]

Premises used: CategoryTheory.Iso.app_inv, CategoryTheory.Functor.mapIso_inv, CategoryTheory.Equivalence.counitInv_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.inverse
-- 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
Y : D
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)
⊢ 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:
slice_lhs 2 3 =>
    dsimp only [Functor.mapIso_inv, Iso.app_inv]
    rw [← map_comp e.inverse, ← e.counitInv_naturality, map_comp]

Premises used: CategoryTheory.Iso.app_inv, CategoryTheory.Functor.mapIso_inv, CategoryTheory.Equivalence.counitInv_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.inverse
-- 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
Y : D
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)))
| 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)))))

Tactic:
rw [e.unitInv_naturality]

Premises used: CategoryTheory.Equivalence.unitInv_naturality
-- 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
Y : D
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)
⊢ 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 3 4 => rw [e.unitInv_naturality]

Premises used: CategoryTheory.Equivalence.unitInv_naturality
-- 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
Y : D
a : e.inverse.map (e.functor.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (𝟭 C) (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)))

Tactic:
rw [← map_comp e.inverse, ← map_comp e.functor, e.unitIso.hom_inv_id_app]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Equivalence.functor, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.inverse
-- 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
Y : D
a : e.inverse.map (e.functor.map (𝟙 (e.inverse.obj Y)))
| e.inverse.map (e.functor.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (𝟭 C) (e.inverse.obj Y))))

Tactic:
dsimp only [Functor.id_obj]

Premises used: CategoryTheory.Functor.id_obj
-- 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
Y : D
a : 𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))
| e.inverse.map (e.functor.map (𝟙 (e.inverse.obj Y)))

Tactic:
rw [map_id, map_id]

Premises used: CategoryTheory.Functor.map_id
-- 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
Y : D
a : 𝟙 (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)))

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]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Equivalence.functor, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.inverse
-- 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
Y : D
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)
⊢ 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 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]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Equivalence.functor, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.inverse
-- 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
Y : D
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)
⊢ 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:
rw [id_comp]

Premises used: CategoryTheory.Category.id_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
Y : D
a : e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y))) ≫ e.unitInv.app (e.inverse.obj Y)
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y)

Tactic:
rw [← e.unitInv_naturality]

Premises used: CategoryTheory.Equivalence.unitInv_naturality
-- 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
Y : D
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)
⊢ 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:
slice_lhs 3 4 => rw [← e.unitInv_naturality]

Premises used: CategoryTheory.Equivalence.unitInv_naturality
-- 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
Y : D
a : e.inverse.map (𝟙 ((e.inverse ⋙ e.functor).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)))

Tactic:
rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_app]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Equivalence.counitInv_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.counitIso, CategoryTheory.Equivalence.inverse
-- 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
Y : D
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)
⊢ 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 2 3 =>
    rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_app]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Equivalence.counitInv_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.counitIso, CategoryTheory.Equivalence.inverse
-- 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
Y : D
⊢ 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:
simp
-- 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
Y : D
⊢ e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)

Tactic:
simpa using Iso.comp_hom_eq_id (e.inverse.mapIso (e.counitIso.app Y)) (f := e.unit.app _)

Premises used: CategoryTheory.Iso.comp_hom_eq_id, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Equivalence.counitIso, CategoryTheory.Equivalence.inverse
-- 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 Y : D
f : X ⟶ Y
⊢ e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counitInv.app Y

Tactic:
(NatIso.naturality_2 e.counitIso f).symm

Premises used: CategoryTheory.NatIso.naturality_2, Eq.symm, CategoryTheory.Equivalence.counitIso
-- 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 Y : C
f : X ⟶ Y
⊢ e.inverse.map (e.functor.map f) = e.unitInv.app X ≫ f ≫ e.unit.app Y

Tactic:
(NatIso.naturality_1 e.unitIso f).symm

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.NatIso.naturality_1, Eq.symm
-- Module: Mathlib.CategoryTheory.Equivalence
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
⊢ 𝟭 C ≅ F ⋙ G

Tactic:
calc
    𝟭 C ≅ F ⋙ G := η
    _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm
    _ ≅ F ⋙ (G ⋙ F) ⋙ G := isoWhiskerLeft F (isoWhiskerRight ε.symm G)
    _ ≅ F ⋙ G ⋙ F ⋙ G := isoWhiskerLeft F (associator G F G)
    _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm
    _ ≅ 𝟭 C ⋙ F ⋙ G := isoWhiskerRight η.symm (F ⋙ G)
    _ ≅ F ⋙ G := leftUnitor (F ⋙ G)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Functor.associator, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.symm, CategoryTheory.Functor.isoWhiskerRight
-- Module: Mathlib.CategoryTheory.Equivalence
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
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)
⊢ F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
dsimp [adjointifyη, Trans.trans]

Premises used: CategoryTheory.Equivalence.adjointifyη, Trans.trans
-- Module: Mathlib.CategoryTheory.Equivalence
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
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)
⊢ 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:
simp only [comp_id, assoc, map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ (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))
-- Module: Mathlib.CategoryTheory.Equivalence
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)
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)
⊢ 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:
rw [this]
-- Module: Mathlib.CategoryTheory.Equivalence
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
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)
⊢ 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 _)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Equivalence
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
⊢ 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)
-- Module: Mathlib.CategoryTheory.Equivalence
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))
rw : F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (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)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Equivalence
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Equivalence
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)))
rw : F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (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)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Equivalence
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
rw : F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
⊢ F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp