-- 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₂)
w : ι₁ ⊕ ι₂
inl :
  ∀ (val : ι₁),
    Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
      ((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 ≫
        (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inl val))
      (s.proj (Sum.inl val))
⊢ (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 ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj w =
    s.proj w
have inr : ∀ (val : ι₂),
  Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
    ((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 ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inr val))
    (s.proj (Sum.inr val))
Tactic: cases w
Cleared hypotheses: w