∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {ι₁ : Type u_3} {ι₂ : Type u_4} {f₁ : ι₁ → C}
  {f₂ : ι₂ → C} {c₁ : CategoryTheory.Limits.Fan f₁} {c₂ : CategoryTheory.Limits.Fan f₂}
  {bc : CategoryTheory.Limits.BinaryFan c₁.pt c₂.pt} (h₁ : CategoryTheory.Limits.IsLimit c₁)
  (h₂ : CategoryTheory.Limits.IsLimit c₂) (h : CategoryTheory.Limits.IsLimit bc)
  (s : CategoryTheory.Limits.Fan (Sum.elim f₁ f₂))
  (m : s.pt ⟶ (CategoryTheory.Limits.Fan.mk bc.pt (c₁.combPairHoms c₂ bc)).pt),
  (∀ (j : ι₁ ⊕ ι₂),
      CategoryTheory.CategoryStruct.comp m ((CategoryTheory.Limits.Fan.mk bc.pt (c₁.combPairHoms c₂ bc)).proj j) =
        s.proj j) →
    ∀ (w : CategoryTheory.Limits.WalkingPair),
      CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Fan.proj bc w) =
        CategoryTheory.CategoryStruct.comp
          ((fun s =>
              CategoryTheory.Limits.Fan.IsLimit.lift h fun i =>
                CategoryTheory.Limits.WalkingPair.casesOn (motive := fun t =>
                  i = t → (s.pt ⟶ CategoryTheory.Limits.WalkingPair.casesOn i c₁.pt c₂.pt)) i
                  (fun h => ⋯ ▸ CategoryTheory.Limits.Fan.IsLimit.lift h₁ fun a => s.proj (Sum.inl a))
                  (fun h => ⋯ ▸ CategoryTheory.Limits.Fan.IsLimit.lift h₂ fun a => s.proj (Sum.inr a)) ⋯)
            s)
          (CategoryTheory.Limits.Fan.proj bc w)