-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y Z : FormalCoproduct.{w, u} C
f : X ⟶ Z
g : Y ⟶ Z
pb : (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i : X.I × Y.I).1 ≫ eqToHom ⋯) (g.φ (↑i : X.I × Y.I).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct.{w, u} C
s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }
a :
  ∀ (x : T.I),
    Hom.f.{w, v, u}
        (↑((fun (m : T ⟶ (pullbackCone f g pb).pt) ↦
                  (Subtype.mk (p := fun (p : (T ⟶ X) × (T ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g)
                      (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) ⋯ :
                    { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }))
                ((fun (s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }) ↦
                    ({
                        f := fun (i : T.I) ↦
                          Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                            ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯,
                        φ := fun (i : T.I) ↦
                          IsLimit.lift
                            (hpb
                              ((fun (i : T.I) ↦
                                  (Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                                      ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯ :
                                    { p : X.I × Y.I // f.f p.1 = g.f p.2 }))
                                i))
                            (PullbackCone.mk ((↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i) ((↑s : (T ⟶ X) × (T ⟶ Y)).2.φ i) ⋯) } :
                      Hom.{w, v, u} T (pullbackCone f g pb).pt))
                  s)) :
            (T ⟶ X) × (T ⟶ Y)).1
        x =
      (↑s : (T ⟶ X) × (T ⟶ Y)).1.f x
a₁ :
  ∀ (i : T.I),
    CategoryStruct.comp (Y :=
        X.obj
          (Hom.f.{w, v, u}
            (↑((fun (m : T ⟶ (pullbackCone f g pb).pt) ↦
                      (Subtype.mk (p := fun (p : (T ⟶ X) × (T ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g)
                          (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) ⋯ :
                        { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }))
                    ((fun (s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }) ↦
                        ({
                            f := fun (i : T.I) ↦
                              Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                                ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯,
                            φ := fun (i : T.I) ↦
                              IsLimit.lift
                                (hpb
                                  ((fun (i : T.I) ↦
                                      (Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                                          ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯ :
                                        { p : X.I × Y.I // f.f p.1 = g.f p.2 }))
                                    i))
                                (PullbackCone.mk ((↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i) ((↑s : (T ⟶ X) × (T ⟶ Y)).2.φ i)
                                  ⋯) } :
                          Hom.{w, v, u} T (pullbackCone f g pb).pt))
                      s)) :
                (T ⟶ X) × (T ⟶ Y)).1
            i))
        (Hom.φ
          (↑((fun (m : T ⟶ (pullbackCone f g pb).pt) ↦
                    (Subtype.mk (p := fun (p : (T ⟶ X) × (T ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g)
                        (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) ⋯ :
                      { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }))
                  ((fun (s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }) ↦
                      ({
                          f := fun (i : T.I) ↦
                            Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                              ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯,
                          φ := fun (i : T.I) ↦
                            IsLimit.lift
                              (hpb
                                ((fun (i : T.I) ↦
                                    (Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                                        ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯ :
                                      { p : X.I × Y.I // f.f p.1 = g.f p.2 }))
                                  i))
                              (PullbackCone.mk ((↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i) ((↑s : (T ⟶ X) × (T ⟶ Y)).2.φ i) ⋯) } :
                        Hom.{w, v, u} T (pullbackCone f g pb).pt))
                    s)) :
              (T ⟶ X) × (T ⟶ Y)).1
          i)
        (eqToHom ⋯) =
      (↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i
⊢ (fun (m : T ⟶ (pullbackCone f g pb).pt) ↦
        (Subtype.mk (p := fun (p : (T ⟶ X) × (T ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g)
            (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) ⋯ :
          { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }))
      ((fun (s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }) ↦
          ({
              f := fun (i : T.I) ↦
                Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                  ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯,
              φ := fun (i : T.I) ↦
                IsLimit.lift
                  (hpb
                    ((fun (i : T.I) ↦
                        (Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                            ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) ⋯ :
                          { p : X.I × Y.I // f.f p.1 = g.f p.2 }))
                      i))
                  (PullbackCone.mk ((↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i) ((↑s : (T ⟶ X) × (T ⟶ Y)).2.φ i) ⋯) } :
            Hom.{w, v, u} T (pullbackCone f g pb).pt))
        s) =
    s
have a₂ : ∀ (x : T.I),
  Hom.f.{w, v, u}
      (↑((fun (m : T ⟶ (pullbackCone f g pb).pt) ↦
                (Subtype.mk (p := fun (p : (T ⟶ X) × (T ⟶ Y)) ↦ p.1 ≫ f = p.2 ≫ g)
                    (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) sorry :
                  { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }))
              ((fun (s : { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }) ↦
                  ({
                      f := fun (i : T.I) ↦
                        Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                          ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) sorry,
                      φ := fun (i : T.I) ↦
                        IsLimit.lift
                          (hpb
                            ((fun (i : T.I) ↦
                                (Subtype.mk (p := fun (p : X.I × Y.I) ↦ f.f p.1 = g.f p.2)
                                    ((↑s : (T ⟶ X) × (T ⟶ Y)).1.f i, (↑s : (T ⟶ X) × (T ⟶ Y)).2.f i) sorry :
                                  { p : X.I × Y.I // f.f p.1 = g.f p.2 }))
                              i))
                          (PullbackCone.mk ((↑s : (T ⟶ X) × (T ⟶ Y)).1.φ i) ((↑s : (T ⟶ X) × (T ⟶ Y)).2.φ i) sorry) } :
                    Hom.{w, v, u} T (pullbackCone f g pb).pt))
                s)) :
          (T ⟶ X) × (T ⟶ Y)).2
      x =
    (↑s : (T ⟶ X) × (T ⟶ Y)).2.f x
Tactic: ext