-- 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 : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} C' D'
X Y : StructuredArrow S T × StructuredArrow S' T'
f : X ⟶ Y
h₁ :
  Eq (α :=
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).1.right ⟶
      (Functor.obj (𝟭 (StructuredArrow S T × StructuredArrow S' T')) Y).1.right)
    (Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
          Iso.hom
            ((fun (f : StructuredArrow S T × StructuredArrow 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)
    (Hom.right
      (Iso.hom
            ((fun (f : StructuredArrow S T × StructuredArrow 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 (𝟭 (StructuredArrow S T × StructuredArrow S' T')) f).1)
⊢ Eq (α :=
    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X ⟶
      Functor.obj (𝟭 (StructuredArrow S T × StructuredArrow S' T')) Y)
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
      Iso.hom
        ((fun (f : StructuredArrow S T × StructuredArrow 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 : StructuredArrow S T × StructuredArrow 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 (𝟭 (StructuredArrow S T × StructuredArrow S' T')) f)
have h₂ : Eq (α :=
  ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).2.right ⟶
    (Functor.obj (𝟭 (StructuredArrow S T × StructuredArrow S' T')) Y).2.right)
  (Hom.right
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
        Iso.hom
          ((fun (f : StructuredArrow S T × StructuredArrow 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)
  (Hom.right
    (Iso.hom
          ((fun (f : StructuredArrow S T × StructuredArrow 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 (𝟭 (StructuredArrow S T × StructuredArrow S' T')) f).2)
Tactic: ext