-- 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₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
w : WalkingPair
left :
  inj bc WalkingPair.left ≫ m =
    inj bc WalkingPair.left ≫
      (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
⊢ inj bc w ≫ m =
    inj bc 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
have right : inj bc WalkingPair.right ≫ m =
  inj bc WalkingPair.right ≫
    (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
Tactic: cases w
Cleared hypotheses: w