-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
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₂
⊢ 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 ⋯)))
have 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 sorry)))).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 sorry))))
      (StructuredArrow.hom
        (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₁)))
          (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom sorry)))
      ((w.costructuredArrowRightwards X₃).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left) sorry))))
  (CommaMorphism.left
    (StructuredArrow.hom
      (StructuredArrow.mk (Y := CostructuredArrow.mk (StructuredArrow.Hom.right (CostructuredArrow.hom f₂)))
        (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom sorry))))
Tactic: ext