awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
C : Type u₁
D : Type u₂
inst_2 : Category.{v₁, u₁} C
inst_3 : Category.{v₂, u₂} D
functor : Functor.{v₁, v₂, u₁, u₂} C D
inverse : Functor.{v₂, v₁, u₂, u₁} D C
unitIso : 𝟭 C ≅ functor ⋙ inverse
counitIso : inverse ⋙ functor ≅ 𝟭 D
functor_unitIso_comp :
  ∀ (X : C), counitIso.inv.app (functor.obj X) ≫ functor.map (unitIso.inv.app X) = 𝟙 (functor.obj X)
X : C
⊢ functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 𝟙 (functor.obj X)

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

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.trans, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.Iso.inv_eq_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
X : C
⊢ e.unit.app X ≫ e.unitInv.app X = 𝟙 X

Tactic:
e.unitIso.hom_inv_id_app X

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Iso.hom_inv_id_app
-- 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.unitInv.app X ≫ e.unit.app X = 𝟙 (e.inverse.obj (e.functor.obj X))

Tactic:
e.unitIso.inv_hom_id_app X

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Iso.inv_hom_id_app
-- 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.counit.app Y ≫ e.counitInv.app Y = 𝟙 (e.functor.obj (e.inverse.obj Y))

Tactic:
e.counitIso.hom_inv_id_app Y

Premises used: CategoryTheory.Iso.hom_inv_id_app, 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
Y : D
⊢ e.counitInv.app Y ≫ e.counit.app Y = 𝟙 Y

Tactic:
e.counitIso.inv_hom_id_app Y

Premises used: CategoryTheory.Iso.inv_hom_id_app, 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 f : Equivalence.{v₁, v₂, u₁, u₂} C D
α β : e ⟶ f
h : asNatTrans α = asNatTrans β
⊢ α = β

Tactic:
h

Premises used: CategoryTheory.Equivalence.asNatTrans
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e f : Equivalence.{v₁, v₂, u₁, u₂} C D
η : e.functor ⟶ f.functor
⊢ mkHom (asNatTrans η) = η

Tactic:
rfl

Premises used: CategoryTheory.Equivalence.asNatTrans, rfl, CategoryTheory.Equivalence.mkHom
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e f : Equivalence.{v₁, v₂, u₁, u₂} C D
η : e ⟶ f
⊢ asNatTrans (mkHom η) = η

Tactic:
rfl

Premises used: CategoryTheory.Equivalence.asNatTrans, rfl, CategoryTheory.Equivalence.mkHom
-- 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
⊢ asNatTrans (𝟙 e) = 𝟙 e.functor

Tactic:
rfl

Premises used: CategoryTheory.Equivalence.asNatTrans, rfl
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e f g : Equivalence.{v₁, v₂, u₁, u₂} C D
α : e ⟶ f
β : f ⟶ g
⊢ asNatTrans (α ≫ β) = asNatTrans α ≫ asNatTrans β

Tactic:
rfl

Premises used: CategoryTheory.Equivalence.asNatTrans, rfl
-- 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
⊢ mkHom (𝟙 e.functor) = 𝟙 e

Tactic:
rfl

Premises used: rfl, CategoryTheory.Equivalence.mkHom
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e f g : Equivalence.{v₁, v₂, u₁, u₂} C D
α : e.functor ⟶ f.functor
β : f.functor ⟶ g.functor
⊢ mkHom (α ≫ β) = mkHom α ≫ mkHom β

Tactic:
rfl

Premises used: rfl, CategoryTheory.Equivalence.mkHom
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
functor : Functor.{v₁, v₂, u₁, u₂} C D
inverse : Functor.{v₂, v₁, u₂, u₁} D C
unit_iso : 𝟭 C ≅ functor ⋙ inverse
counit_iso : inverse ⋙ functor ≅ 𝟭 D
f : ∀ (X : C), functor.map (unit_iso.hom.app X) ≫ counit_iso.hom.app (functor.obj X) = 𝟙 (functor.obj X)
⊢ { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f :
        Equivalence.{v₁, v₂, u₁, u₂} C D }.unit =
    unit_iso.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
functor : Functor.{v₁, v₂, u₁, u₂} C D
inverse : Functor.{v₂, v₁, u₂, u₁} D C
unit_iso : 𝟭 C ≅ functor ⋙ inverse
counit_iso : inverse ⋙ functor ≅ 𝟭 D
f : ∀ (X : C), functor.map (unit_iso.hom.app X) ≫ counit_iso.hom.app (functor.obj X) = 𝟙 (functor.obj X)
⊢ { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f :
        Equivalence.{v₁, v₂, u₁, u₂} C D }.counit =
    counit_iso.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
functor : Functor.{v₁, v₂, u₁, u₂} C D
inverse : Functor.{v₂, v₁, u₂, u₁} D C
unit_iso : 𝟭 C ≅ functor ⋙ inverse
counit_iso : inverse ⋙ functor ≅ 𝟭 D
f : ∀ (X : C), functor.map (unit_iso.hom.app X) ≫ counit_iso.hom.app (functor.obj X) = 𝟙 (functor.obj X)
⊢ { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f :
        Equivalence.{v₁, v₂, u₁, u₂} C D }.unitInv =
    unit_iso.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
functor : Functor.{v₁, v₂, u₁, u₂} C D
inverse : Functor.{v₂, v₁, u₂, u₁} D C
unit_iso : 𝟭 C ≅ functor ⋙ inverse
counit_iso : inverse ⋙ functor ≅ 𝟭 D
f : ∀ (X : C), functor.map (unit_iso.hom.app X) ≫ counit_iso.hom.app (functor.obj X) = 𝟙 (functor.obj X)
⊢ { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f :
        Equivalence.{v₁, v₂, u₁, u₂} C D }.counitInv =
    counit_iso.inv

Tactic:
rfl

Premises used: rfl
-- 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 Y = e.counit.app X ≫ f

Tactic:
e.counit.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Equivalence.counit
-- 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.unit.app X ≫ e.inverse.map (e.functor.map f) = f ≫ e.unit.app Y

Tactic:
(e.unit.naturality f).symm

Premises used: CategoryTheory.Equivalence.unit, CategoryTheory.NatTrans.naturality, Eq.symm
-- 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.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X)

Tactic:
e.functor_unitIso_comp X

Premises used: CategoryTheory.Equivalence.functor_unitIso_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.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)

Tactic:
simpa using Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)) (f := e.counit.app _)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Equivalence.functor, CategoryTheory.Iso.app, CategoryTheory.Iso.hom_comp_eq_id, CategoryTheory.Functor.mapIso
-- 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.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.counit.app Y) = 𝟙 (e.inverse.obj Y)

Tactic:
rw [← id_comp (e.inverse.map _), ← map_id e.inverse, ← counitInv_functor_comp, map_comp]

Premises used: CategoryTheory.Equivalence.counitInv_functor_comp, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_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.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)
⊢ 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 [← Iso.hom_inv_id_assoc (e.unitIso.app _) (e.inverse.map (e.functor.map _)), Iso.app_hom,
    Iso.app_inv]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Iso.app_inv, CategoryTheory.Equivalence.functor, CategoryTheory.Iso.app_hom, CategoryTheory.Functor.map, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Iso.app, 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.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.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)))))

Tactic:
rw [← e.unit_naturality]

Premises used: CategoryTheory.Equivalence.unit_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.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)
⊢ 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:
slice_lhs 2 3 => rw [← e.unit_naturality]

Premises used: CategoryTheory.Equivalence.unit_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.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))
| e.unit.app (e.inverse.obj Y) ≫ e.unit.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))

Tactic:
rw [← e.unit_naturality]

Premises used: CategoryTheory.Equivalence.unit_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.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)
⊢ 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 1 2 => rw [← e.unit_naturality]

Premises used: CategoryTheory.Equivalence.unit_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 :
  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.unitIso.inv.app (e.inverse.1 (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 _)]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Equivalence.unitInv, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.NatTrans.app, 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.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)
⊢ ((((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 4 4 =>
    rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Equivalence.unitInv, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.NatTrans.app, 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
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)))))
| 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))))))

Tactic:
dsimp only [Functor.mapIso_hom, Iso.app_hom]

Premises used: CategoryTheory.Iso.app_hom, CategoryTheory.Functor.mapIso_hom
-- 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.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)))))
| 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:
rw [← map_comp e.inverse]

Premises used: 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.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)))))
| 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:
dsimp
-- 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 (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.counitIso.hom.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

Tactic:
rw [e.counit_naturality, e.counitIso.hom_inv_id_app]

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

Tactic:
dsimp only [Functor.comp_obj]

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

Tactic:
rw [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 (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))))) ≫
    Iso.hom (e.inverse.mapIso (e.counitIso.app (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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Iso.app_hom, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.mapIso_hom, CategoryTheory.Equivalence.counit_naturality, 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.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.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 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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Iso.app_hom, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.mapIso_hom, CategoryTheory.Equivalence.counit_naturality, CategoryTheory.Equivalence.counitIso, CategoryTheory.Equivalence.inverse