-- Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean
lemma vComp_iff_of_equivalences (eL : C₂ ≌ C₃) (eR : D₂ ≌ D₃)
    (w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃) :
    (w ≫ᵥ w'.hom).GuitartExact ↔ w.GuitartExact

Proof state:
case h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_7, u_2} C₂
inst✝³ : Category.{u_8, u_3} C₃
inst✝² : Category.{u_12, u_4} D₁
inst✝¹ : Category.{u_9, u_5} D₂
inst✝ : Category.{u_10, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso' := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ isoWhiskerLeft L₁ eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ isoWhiskerLeft R₁ eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map ((natTrans w'.hom).app (L₁.obj X₁)) ≫
          (natTrans (CatCommSq.iso H₃ eL.inverse eR.inverse H₂).hom).app (eL.functor.obj (L₁.obj X₁)) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))

Tactic:
erw [CatCommSq.vInv_iso'_hom_app]

Result:
case h
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_7, u_2} C₂
inst✝³ : Category.{u_8, u_3} C₃
inst✝² : Category.{u_12, u_4} D₁
inst✝¹ : Category.{u_9, u_5} D₂
inst✝ : Category.{u_10, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso' := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ isoWhiskerLeft L₁ eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ isoWhiskerLeft R₁ eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map ((natTrans w'.hom).app (L₁.obj X₁)) ≫
          (eR.inverse.map (H₃.map (eL.counitIso.inv.app (eL.functor.obj (L₁.obj X₁)))) ≫
              eR.inverse.map
                  ((CatCommSq.iso H₂ eL.functor eR.functor H₃).inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
                eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁))))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_7, u_2} C₂
inst✝³ : Category.{u_8, u_3} C₃
inst✝² : Category.{u_12, u_4} D₁
inst✝¹ : Category.{u_9, u_5} D₂
inst✝ : Category.{u_10, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso' := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
⊢ w.GuitartExact

Tactic:
let w'' := CatCommSq.iso H₃ eL.inverse eR.inverse H₂

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_7, u_2} C₂
inst✝³ : Category.{u_8, u_3} C₃
inst✝² : Category.{u_12, u_4} D₁
inst✝¹ : Category.{u_9, u_5} D₂
inst✝ : Category.{u_10, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso' := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
⊢ w.GuitartExact

Proof state:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_7, u_2} C₂
inst✝³ : Category.{u_8, u_3} C₃
inst✝² : Category.{u_12, u_4} D₁
inst✝¹ : Category.{u_9, u_5} D₂
inst✝ : Category.{u_10, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso' := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ isoWhiskerLeft L₁ eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ isoWhiskerLeft R₁ eR.unitIso.symm ≪≫ R₁.rightUnitor
⊢ w.GuitartExact

Tactic:
have : w = (w ≫ᵥ w'.hom).vComp' w''.hom α β := by
  ext X₁
  dsimp
  simp? [w'', α, β] says
    simp only [vComp'_app, Functor.comp_obj, Iso.trans_inv, isoWhiskerLeft_inv, Iso.symm_inv,
      assoc, NatTrans.comp_app, Functor.id_obj, Functor.rightUnitor_inv_app,
      CategoryTheory.whiskerLeft_app, Functor.associator_inv_app, comp_id, id_comp, vComp_app,
      Functor.map_comp, Equivalence.inv_fun_map, Iso.trans_hom, isoWhiskerLeft_hom,
      Iso.symm_hom, Functor.associator_hom_app, Functor.rightUnitor_hom_app,
      Iso.hom_inv_id_app_assoc, w'', α, β]
  erw [CatCommSq.vInv_iso'_hom_app]
  simp only [CategoryTheory.whiskerLeft_app, Iso.hom_inv_id_app_assoc,
    hw', assoc, ← eR.inverse.map_comp_assoc]
  rw [Equivalence.counitInv_app_functor]
  erw [← NatTrans.naturality_assoc]
  simp [← H₂.map_comp]

Result:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_7, u_2} C₂
inst✝³ : Category.{u_8, u_3} C₃
inst✝² : Category.{u_12, u_4} D₁
inst✝¹ : Category.{u_9, u_5} D₂
inst✝ : Category.{u_10, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝¹ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso' := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this✝ : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ isoWhiskerLeft L₁ eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ isoWhiskerLeft R₁ eR.unitIso.symm ≪≫ R₁.rightUnitor
this : w = (w ≫ᵥ w'.hom).vComp' w''.hom α β
⊢ w.GuitartExact