-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} C' D'
T : D
T' : D'
X Y : CostructuredArrow S T × CostructuredArrow S' T'
f : X ⟶ Y
h₁ :
  Eq (α :=
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).1.left ⟶
      (Functor.obj (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) Y).1.left)
    (CommaMorphism.left
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
          Iso.hom
            ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              Y)).1)
    (CommaMorphism.left
      (Iso.hom
            ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              X) ≫
          Functor.map (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) f).1)
⊢ Eq (α :=
    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X ⟶
      Functor.obj (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) Y)
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
      Iso.hom
        ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
            (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
              (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
          Y))
    (Iso.hom
        ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
            (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
              (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
          X) ≫
      Functor.map (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) f)
have h₂ : Eq (α :=
  ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).2.left ⟶
    (Functor.obj (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) Y).2.left)
  (CommaMorphism.left
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
        Iso.hom
          ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
              (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
            Y)).2)
  (CommaMorphism.left
    (Iso.hom
          ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
              (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
            X) ≫
        Functor.map (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) f).2)
Tactic: ext