-- 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₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
m : s.pt ⟶ (mk bc.pt (c₁.combPairHoms c₂ bc)).pt
hm : ∀ (j : ι₁ ⊕ ι₂), m ≫ (mk bc.pt (c₁.combPairHoms c₂ bc)).proj j = s.proj j
w : WalkingPair
left :
  m ≫ proj bc WalkingPair.left =
    (fun (s : Fan (Sum.elim f₁ f₂)) ↦
          (IsLimit.lift h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
                ⋯ :
            s.pt ⟶ bc.pt))
        s ≫
      proj bc WalkingPair.left
⊢ m ≫ proj bc w =
    (fun (s : Fan (Sum.elim f₁ f₂)) ↦
          (IsLimit.lift h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
                ⋯ :
            s.pt ⟶ bc.pt))
        s ≫
      proj bc w
have right : m ≫ proj bc WalkingPair.right =
  (fun (s : Fan (Sum.elim f₁ f₂)) ↦
        (IsLimit.lift h fun (i : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
              (h : i = t) → s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt) i
              (fun (h : i = WalkingPair.left) ↦
                Eq.ndrec (motive := fun (i : WalkingPair) ↦
                  s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                  (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) sorry)
              (fun (h : i = WalkingPair.right) ↦
                Eq.ndrec (motive := fun (i : WalkingPair) ↦
                  s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                  (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) sorry)
              sorry :
          s.pt ⟶ bc.pt))
      s ≫
    proj bc WalkingPair.right
Tactic: cases w
Cleared hypotheses: w