-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
w : ι₁ ⊕ ι₂
inl :
  ∀ (val : ι₁),
    Eq (α := Sum.elim f₁ f₂ (Sum.inl val) ⟶ s.pt)
      ((mk bc.pt (c₁.combPairHoms c₂ bc)).inj (Sum.inl val) ≫
        (fun (s : Cofan (Sum.elim f₁ f₂)) ↦
            (IsColimit.desc h fun (i : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                  (h : i = t) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt) i
                  (fun (h : i = WalkingPair.left) ↦
                    Eq.ndrec (motive := fun (i : WalkingPair) ↦
                      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                      (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
                  (fun (h : i = WalkingPair.right) ↦
                    Eq.ndrec (motive := fun (i : WalkingPair) ↦
                      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                      (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
                  ⋯ :
              bc.pt ⟶ s.pt))
          s)
      (s.inj (Sum.inl val))
⊢ (mk bc.pt (c₁.combPairHoms c₂ bc)).inj w ≫
      (fun (s : Cofan (Sum.elim f₁ f₂)) ↦
          (IsColimit.desc h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
                ⋯ :
            bc.pt ⟶ s.pt))
        s =
    s.inj w
have inr : ∀ (val : ι₂),
  Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
    ((mk bc.pt (c₁.combPairHoms c₂ bc)).inj (Sum.inr val) ≫
      (fun (s : Cofan (Sum.elim f₁ f₂)) ↦
          (IsColimit.desc h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) sorry)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) sorry)
                sorry :
            bc.pt ⟶ s.pt))
        s)
    (s.inj (Sum.inr val))
Tactic: cases w
Cleared hypotheses: w