-- Mathlib/CategoryTheory/Equivalence.lean
theorem unit_inverse_comp (e : C ≌ D) (Y : D) :
    e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ ((((e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ (e.functor ⋙ e.inverse).map (e.unit.1 (e.inverse.obj Y))) ≫
            (e.functor ⋙ e.inverse).map
              (e.inverse.toPrefunctor.2 (e.counitInv.app (e.functor.obj (e.inverse.obj Y))))) ≫
          e.unitIso.inv.app
            (e.inverse.toPrefunctor.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 _)]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      (e.functor ⋙ e.inverse).map (e.unit.1 (e.inverse.obj Y)) ≫
        (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))) ≫
          (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).hom ≫
                (e.inverse.mapIso
                      (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫
                  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)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (e.counit.app Y)) ≫
          e.unitInv.app (e.inverse.toPrefunctor.1 Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
slice_lhs 2 3 =>
  erw [← map_comp e.inverse, ← e.counitIso.inv.naturality, (e.counitIso.app _).hom_inv_id,
    map_id]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      𝟙 (e.inverse.obj (e.functor.obj ((𝟭 C).obj (e.inverse.obj Y)))) ≫ e.unitInv.app (e.inverse.toPrefunctor.1 Y) =
    𝟙 (e.inverse.obj Y)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      (e.functor ⋙ e.inverse).map (e.unit.1 (e.inverse.obj Y)) ≫
        (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫
              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 => erw [← map_comp e.inverse, e.counitIso.inv.naturality, map_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      (((e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
              e.inverse.map ((e.inverse ⋙ e.functor).map (e.functor.toPrefunctor.2 (e.unit.1 (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)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      𝟙 (e.inverse.obj (e.functor.obj ((𝟭 C).obj (e.inverse.obj Y)))) ≫ e.unitInv.app (e.inverse.toPrefunctor.1 Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        e.unitInv.app (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
          𝟙 ((e.functor ⋙ e.inverse).obj ((𝟭 C).obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
erw [id_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        e.unitInv.app (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
          e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      (e.functor ⋙ e.inverse).map (e.unit.1 (e.inverse.obj Y)) ≫
        (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))) ≫
          (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).hom ≫
                (e.inverse.mapIso
                      (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫
                  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 =>
  erw [← map_comp e.inverse, e.counit.naturality]
  erw [(e.counitIso.app _).hom_inv_id, map_id]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      (e.functor ⋙ e.inverse).map (e.unit.1 (e.inverse.obj Y)) ≫
        (((𝟙 (e.inverse.obj (e.functor.obj (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj Y))))) ≫
                (e.inverse.mapIso
                    (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv) ≫
              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)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        e.unitInv.app (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
          e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
slice_lhs 3 4 => erw [← e.unitInv.naturality]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫
      e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (e.counit.app Y)) ≫
          e.unitInv.app (e.inverse.toPrefunctor.1 Y) =
    𝟙 (e.inverse.obj Y)