-- Module: Mathlib.CategoryTheory.GuitartExact.Basic
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
h :
  Eq (α :=
    (CostructuredArrow.mk g).left ⟶
      ((w.costructuredArrowRightwards X₃).obj
          (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
            w.costructuredArrowRightwards X₃)
            (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
              (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯)))).left)
    (CommaMorphism.left
      (CategoryStruct.comp (Y :=
        (w.costructuredArrowRightwards X₃).obj
          (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
            w.costructuredArrowRightwards X₃)
            (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
              (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯))))
        (StructuredArrow.hom
          (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
            (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)))
        ((w.costructuredArrowRightwards X₃).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯))))
    (CommaMorphism.left
      (StructuredArrow.hom
        (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
          (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯))))
⊢ Eq (α :=
    CostructuredArrow.mk g ⟶
      (w.costructuredArrowRightwards X₃).obj
        (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
          w.costructuredArrowRightwards X₃)
          (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
            (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯))))
    (CategoryStruct.comp (Y :=
      (w.costructuredArrowRightwards X₃).obj
        (StructuredArrow.right (D := CostructuredArrow R (B.obj X₃)) (S := CostructuredArrow.mk g) (T :=
          w.costructuredArrowRightwards X₃)
          (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
            (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯))))
      (StructuredArrow.hom
        (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
          (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)))
      ((w.costructuredArrowRightwards X₃).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯)))
    (StructuredArrow.hom
      (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
        (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯)))

Tactic:
ext