-- Mathlib/CategoryTheory/CatCommSq.lean
lemma hInv_hInv (h : CatCommSq T.functor L R B.functor) :
    hInv T.symm R L B.symm (hInv T L R B h) = h

Proof state:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.symm.inverse.obj X))) ≫
              B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.symm.inverse.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.symm.inverse.obj X)))) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      B.functor.map (L.map (T.unitIso.hom.app X)) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ iso'.hom.app ((T.functor ⋙ T.inverse).obj X)

Tactic:
dsimp

Result:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
        B.functor.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.functor.obj X))) ≫
              B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X)))) ≫
          B.functor.map (L.map (T.unitIso.inv.app X))) ≫
      B.functor.map (L.map (T.unitIso.hom.app X)) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫ iso'.hom.app (T.inverse.obj (T.functor.obj X))

Proof state:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ R.map (T.functor.map (T.unit.app X)) ≫ (iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X)) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫ iso'.hom.app (T.inverse.obj (T.functor.obj X))

Tactic:
rfl

Result:
no goals

Proof state:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
        B.functor.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.functor.obj X))) ≫
              B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X)))) ≫
          B.functor.map (L.map (T.unitIso.inv.app X))) ≫
      B.functor.map (L.map (T.unitIso.hom.app X)) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫ iso'.hom.app (T.inverse.obj (T.functor.obj X))

Tactic:
simp only [Functor.comp_obj, assoc, ← Functor.map_comp, Iso.inv_hom_id_app,
  Equivalence.counitInv_app_functor, Functor.map_id]

Result:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
      B.functor.map
        (B.inverse.map (R.map (T.functor.map (T.unit.app X))) ≫
          B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))) ≫
            B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X))) ≫ 𝟙 (L.obj (T.inverse.obj (T.functor.obj X)))) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫ iso'.hom.app (T.inverse.obj (T.functor.obj X))

Proof state:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
      B.functor.map
        (B.inverse.map (R.map (T.functor.map (T.unit.app X))) ≫
          B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))) ≫
            B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X))) ≫ 𝟙 (L.obj (T.inverse.obj (T.functor.obj X)))) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫ iso'.hom.app (T.inverse.obj (T.functor.obj X))

Tactic:
simp only [Functor.map_comp, Equivalence.fun_inv_map, assoc,
  Equivalence.counitInv_functor_comp, comp_id, Iso.inv_hom_id_app_assoc]

Result:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ R.map (T.functor.map (T.unit.app X)) ≫ (iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X)) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫ iso'.hom.app (T.inverse.obj (T.functor.obj X))

Proof state:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ iso'.hom.app X = iso'.hom.app X

Tactic:
erw [← cancel_mono (B.functor.map (L.map (T.unitIso.hom.app X))),
  ← h.iso'.hom.naturality (T.unitIso.hom.app X), hInv_iso'_hom_app, hInv_iso'_inv_app]

Result:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.symm.inverse.obj X))) ≫
              B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.symm.inverse.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.symm.inverse.obj X)))) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      B.functor.map (L.map (T.unitIso.hom.app X)) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ iso'.hom.app ((T.functor ⋙ T.inverse).obj X)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
⊢ hInv T.symm R L B.symm (hInv T L R B h) = h

Tactic:
ext X

Result:
case iso'.w.w.h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{u_8, u_1} C₁
inst✝² : Category.{u_9, u_2} C₂
inst✝¹ : Category.{u_10, u_3} C₃
inst✝ : Category.{u_7, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ iso'.hom.app X = iso'.hom.app X