-- Mathlib/CategoryTheory/CatCommSq.lean
lemma vInv_vInv (h : CatCommSq T L.functor R.functor B) :
    vInv B L.symm R.symm T (vInv 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 L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
        R.counit.app (R.functor.obj (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
          (iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X)) ≫
            B.map (L.counitIso.hom.app (L.functor.obj X)) ≫ B.map (L.functor.map (L.unitIso.hom.app X)) =
    R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      (iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))

Tactic:
erw [← B.map_comp, L.counit_app_functor, ← L.functor.map_comp, ← NatTrans.comp_app,
  Iso.inv_hom_id, NatTrans.id_app, L.functor.map_id, B.map_id, comp_id, R.counit_app_functor,
  ← R.functor.map_comp_assoc, ← R.functor.map_comp_assoc, assoc, ← NatTrans.comp_app,
  Iso.hom_inv_id, NatTrans.id_app, comp_id]

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 L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    iso'.hom.app X

Tactic:
rw [← cancel_mono (B.map (L.functor.map (NatTrans.app L.unitIso.hom 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 L.functor R.functor B
X : C₁
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    iso'.hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app 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 L.functor R.functor B
⊢ vInv B L.symm R.symm T (vInv 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 L.functor R.functor B
X : C₁
⊢ iso'.hom.app X = iso'.hom.app 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 L.functor R.functor B
X : C₁
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    iso'.hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
erw [← (iso T L.functor R.functor B).hom.naturality (L.unitIso.hom.app 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 L.functor R.functor B
X : C₁
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (T ⋙ R.functor).map (L.unitIso.hom.app X) ≫ (iso T L.functor R.functor B).hom.app ((L.functor ⋙ L.inverse).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 L.functor R.functor B
X : C₁
⊢ iso'.hom.app X = iso'.hom.app X

Tactic:
erw [vInv_iso'_hom_app, vInv_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 L.functor R.functor B
X : C₁
⊢ R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫
      R.symm.inverse.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.symm.inverse.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.symm.inverse.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.symm.inverse.obj X)))) ≫
        R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) =
    iso'.hom.app 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 L.functor R.functor B
X : C₁
⊢ R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫
      R.symm.inverse.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.symm.inverse.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.symm.inverse.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.symm.inverse.obj X)))) ≫
        R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) =
    iso'.hom.app 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 L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    iso'.hom.app X