-- 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.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)) =
    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:
simp only [Functor.map_comp, Equivalence.fun_inv_map, Functor.comp_obj,
  Functor.id_obj, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app, comp_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 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))

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)) =
    (T ⋙ R.functor).map (L.unitIso.hom.app X) ≫ (iso T L.functor R.functor B).hom.app ((L.functor ⋙ L.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 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)) =
    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))