awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
⊢ s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.right c₁.pt c₂.pt

Tactic:
exact Fan.IsLimit.lift h₂ (fun a ↦ s.proj (.inr a))

Premises used: CategoryTheory.Limits.Fan.proj, Sum.inr, CategoryTheory.Limits.Fan.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
val : ι₁
inl :
  Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
    ((IsLimit.lift h fun (i : WalkingPair) ↦
        WalkingPair.rec (motive := fun (t : WalkingPair) ↦
          (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
          (fun (h : i = WalkingPair.left) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
          (fun (h : i = WalkingPair.right) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
          i ⋯) ≫
      bc.fst ≫ c₁.proj val)
    (s.proj (Sum.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))

Tactic:
simp only [fan_mk_proj, combPairHoms]

Premises used: CategoryTheory.Limits.Fan.combPairHoms, CategoryTheory.Limits.fan_mk_proj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
val : ι₁
inl :
  Eq.{u₂ + 1} (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
    (NatTrans.app
          (Cone.π
            (mk s.pt fun (i : WalkingPair) ↦
              WalkingPair.rec (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
                (fun (h : i = WalkingPair.left) ↦
                  Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                    s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                    s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
                i ⋯))
          { as := WalkingPair.left } ≫
        c₁.proj val :
      s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
    (s.proj (Sum.inl val) : s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
⊢ Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
    ((IsLimit.lift h fun (i : WalkingPair) ↦
        WalkingPair.rec (motive := fun (t : WalkingPair) ↦
          (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
          (fun (h : i = WalkingPair.left) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
          (fun (h : i = WalkingPair.right) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
          i ⋯) ≫
      bc.fst ≫ c₁.proj val)
    (s.proj (Sum.inl val))

Tactic:
erw [← Category.assoc, h.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
val : ι₁
⊢ Eq.{u₂ + 1} (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
    (NatTrans.app
          (Cone.π
            (mk s.pt fun (i : WalkingPair) ↦
              WalkingPair.rec (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
                (fun (h : i = WalkingPair.left) ↦
                  Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                    s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                    s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
                i ⋯))
          { as := WalkingPair.left } ≫
        c₁.proj val :
      s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
    (s.proj (Sum.inl val) : s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))

Tactic:
simp only [pair_obj_left, mk_pt, mk_π_app, IsLimit.fac]

Premises used: CategoryTheory.Limits.Fan.IsLimit.fac, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.Limits.pair_obj_left, CategoryTheory.Limits.Fan.mk_π_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
val : ι₂
inr :
  Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
    ((IsLimit.lift h fun (i : WalkingPair) ↦
        WalkingPair.rec (motive := fun (t : WalkingPair) ↦
          (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
          (fun (h : i = WalkingPair.left) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
          (fun (h : i = WalkingPair.right) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
          i ⋯) ≫
      bc.snd ≫ c₂.proj val)
    (s.proj (Sum.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)) ⋯)
                (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.inr val))
    (s.proj (Sum.inr val))

Tactic:
simp only [fan_mk_proj, combPairHoms]

Premises used: CategoryTheory.Limits.Fan.combPairHoms, CategoryTheory.Limits.fan_mk_proj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
val : ι₂
inr :
  Eq.{u₂ + 1} (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
    (NatTrans.app
          (Cone.π
            (mk s.pt fun (i : WalkingPair) ↦
              WalkingPair.rec (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
                (fun (h : i = WalkingPair.left) ↦
                  Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                    s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                    s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
                i ⋯))
          { as := WalkingPair.right } ≫
        c₂.proj val :
      s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
    (s.proj (Sum.inr val) : s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
⊢ Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
    ((IsLimit.lift h fun (i : WalkingPair) ↦
        WalkingPair.rec (motive := fun (t : WalkingPair) ↦
          (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
          (fun (h : i = WalkingPair.left) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
          (fun (h : i = WalkingPair.right) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
          i ⋯) ≫
      bc.snd ≫ c₂.proj val)
    (s.proj (Sum.inr val))

Tactic:
erw [← Category.assoc, h.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
val : ι₂
⊢ Eq.{u₂ + 1} (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
    (NatTrans.app
          (Cone.π
            (mk s.pt fun (i : WalkingPair) ↦
              WalkingPair.rec (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
                (fun (h : i = WalkingPair.left) ↦
                  Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                    s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                    s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
                i ⋯))
          { as := WalkingPair.right } ≫
        c₂.proj val :
      s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
    (s.proj (Sum.inr val) : s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))

Tactic:
simp only [pair_obj_left, mk_pt, mk_π_app, IsLimit.fac]

Premises used: CategoryTheory.Limits.Fan.IsLimit.fac, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.Limits.pair_obj_left, CategoryTheory.Limits.Fan.mk_π_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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
a : ι₁
⊢ (m ≫ proj bc WalkingPair.left) ≫ c₁.proj a =
    ((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) ≫
      c₁.proj a

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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
⊢ 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

Tactic:
refine Fan.IsLimit.hom_ext h₁ _ _ (fun a ↦ by aesop)

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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
a : ι₂
⊢ (m ≫ proj bc WalkingPair.right) ≫ c₂.proj a =
    ((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.right) ≫
      c₂.proj a

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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
⊢ 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)) ⋯)
                (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.right

Tactic:
refine Fan.IsLimit.hom_ext h₂ _ _ (fun a ↦ by aesop)

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
i : WalkingPair
left : WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left c₁.pt c₂.pt ⟶ s.pt
right : WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.right c₁.pt c₂.pt ⟶ s.pt
⊢ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt

Tactic:
cases i
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
⊢ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left c₁.pt c₂.pt ⟶ s.pt

Tactic:
exact Cofan.IsColimit.desc h₁ (fun a ↦ s.inj (.inl a))

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, Sum.inl, CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
⊢ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.right c₁.pt c₂.pt ⟶ s.pt

Tactic:
exact Cofan.IsColimit.desc h₂ (fun a ↦ s.inj (.inr a))

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.Limits.Cofan.inj, Sum.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
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₂)
val : ι₁
inl :
  Eq (α := Sum.elim f₁ f₂ (Sum.inl val) ⟶ s.pt)
    (c₁.inj val ≫
      bc.inl ≫
        IsColimit.desc h fun (i : WalkingPair) ↦
          WalkingPair.rec (motive := fun (t : WalkingPair) ↦
            (h : i = t) → WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i ⟶ s.pt)
            (fun (h : i = WalkingPair.left) ↦
              Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
            (fun (h : i = WalkingPair.right) ↦
              Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
            i ⋯)
    (s.inj (Sum.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))

Tactic:
simp only [cofan_mk_inj, combPairHoms, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofan.combPairHoms, CategoryTheory.Limits.cofan_mk_inj