awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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 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)) 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.left
Tactic: cases w
Cleared hypotheses: w
-- 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₂)
i : WalkingPair
⊢ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt
have left : WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left c₁.pt c₂.pt ⟶ s.pt
Tactic: cases i
Cleared hypotheses: i
-- 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₂)
i : WalkingPair
left : WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left c₁.pt c₂.pt ⟶ s.pt
⊢ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt
have right : WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.right c₁.pt c₂.pt ⟶ s.pt
Tactic: cases i
Cleared hypotheses: i
-- 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₂)
w : ι₁ ⊕ ι₂
⊢ (mk bc.pt (c₁.combPairHoms c₂ bc)).inj 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 =
    s.inj w
have 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)) 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)
    (s.inj (Sum.inl val))
Tactic: cases w
Cleared hypotheses: w
-- 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₂)
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))
have 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)) sorry)
          (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)) sorry)
          i sorry)
  (s.inj (Sum.inl val))
Tactic: simp only [cofan_mk_inj, combPairHoms, Category.assoc]
-- 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₂)
val : ι₁
⊢ 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))
have inl : Eq (α := Sum.elim f₁ f₂ (Sum.inl val) ⟶ s.pt)
  (c₁.inj val ≫
    NatTrans.app
      (Cocone.ι
        (mk s.pt 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)) sorry)
            (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)) sorry)
            i sorry))
      { as := WalkingPair.left })
  (s.inj (Sum.inl val))
Tactic: erw [h.fac]
-- 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₂)
val : ι₂
⊢ Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
    ((mk bc.pt (c₁.combPairHoms c₂ bc)).inj (Sum.inr 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.inr val))
have inr : Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
  (c₂.inj val ≫
    bc.inr ≫
      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)) sorry)
          (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)) sorry)
          i sorry)
  (s.inj (Sum.inr val))
Tactic: simp only [cofan_mk_inj, combPairHoms, Category.assoc]
-- 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₂)
val : ι₂
⊢ Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
    (c₂.inj val ≫
      bc.inr ≫
        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.inr val))
have inr : Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
  (c₂.inj val ≫
    NatTrans.app
      (Cocone.ι
        (mk s.pt 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)) sorry)
            (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)) sorry)
            i sorry))
      { as := WalkingPair.right })
  (s.inj (Sum.inr val))
Tactic: erw [h.fac]
-- 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
⊢ 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 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)) 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
J : Type w
F : J → C
inst_3 : HasProduct.{w, v, u} F
inst_4 : PreservesLimit (Discrete.functor F) (forget C (FC := FC) (CC := CC))
x : (j : J) → ToType (FC := FC) (CC := CC) (F j)
j : J
⊢ (hom (FC := FC) (CC := CC) (Pi.π F j) : (a : CC (∏ᶜ F)) → CC (F j))
      ((Equiv.symm (productEquiv (FC := FC) (CC := CC) F) : (a : (j : J) → ToType (F j)) → ToType (∏ᶜ F)) x) =
    x j
have rw : (productEquiv (FC := FC) (CC := CC) F : (a : ToType (∏ᶜ F)) → (j : J) → ToType (F j))
    ((Equiv.symm (productEquiv (FC := FC) (CC := CC) F) : (a : (j : J) → ToType (F j)) → ToType (∏ᶜ F)) x :
      ToType (FC := FC) (CC := CC) (piObj.{w, v, u} F))
    j =
  x j
Tactic: rw [← productEquiv_apply_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
J : Type w
F : J → C
inst_3 : HasProduct.{w, v, u} F
inst_4 : PreservesLimit (Discrete.functor F) (forget C (FC := FC) (CC := CC))
x : (j : J) → ToType (FC := FC) (CC := CC) (F j)
j : J
rw :
  (productEquiv (FC := FC) (CC := CC) F : (a : ToType (∏ᶜ F)) → (j : J) → ToType (F j))
      ((Equiv.symm (productEquiv (FC := FC) (CC := CC) F) : (a : (j : J) → ToType (F j)) → ToType (∏ᶜ F)) x :
        ToType (FC := FC) (CC := CC) (piObj.{w, v, u} F))
      j =
    x j
⊢ (hom (FC := FC) (CC := CC) (Pi.π F j) : (a : CC (∏ᶜ F)) → CC (F j))
      ((Equiv.symm (productEquiv (FC := FC) (CC := CC) F) : (a : (j : J) → ToType (F j)) → ToType (∏ᶜ F)) x) =
    x j
have rw₁ : x j = x j
Tactic: rw [← productEquiv_apply_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
f : J → C
inst_1 : HasProduct.{w, v, u} f
D : Type t
inst_2 : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst_3 : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst_4 : ConcreteCategory D FD (CC := DD)
F : Functor.{v, r, u, t} C D
inst_5 : PreservesLimit (Discrete.functor f) F
inst_6 : HasProduct.{w, r, t} (C := D) fun (j : J) ↦ F.obj (f j)
inst_7 : PreservesLimitsOfShape WalkingCospan (forget D (FC := FD) (CC := DD))
inst_8 : PreservesLimit (J := Discrete J) (Discrete.functor fun (b : J) ↦ F.obj (f b)) (forget D (FC := FD) (CC := DD))
x y : ToType (FC := FD) (CC := DD) (F.obj (piObj.{w, v, u} f))
h :
  ∀ (i : J),
    Eq (α := DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) x : DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) y : DD (F.obj (f i)))
⊢ x = y
have a : Eq (α := DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
  ((hom (FC := FD) (CC := DD) (Iso.hom (PreservesProduct.iso F f)) :
        (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (j : J) ↦ F.obj (f j)))
      x :
    DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
  ((hom (FC := FD) (CC := DD) (Iso.hom (PreservesProduct.iso F f)) :
        (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (j : J) ↦ F.obj (f j)))
      y :
    DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
Tactic: apply ConcreteCategory.injective_of_mono_of_preservesPullback (PreservesProduct.iso F f).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
f : J → C
inst_1 : HasProduct.{w, v, u} f
D : Type t
inst_2 : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst_3 : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst_4 : ConcreteCategory D FD (CC := DD)
F : Functor.{v, r, u, t} C D
inst_5 : PreservesLimit (Discrete.functor f) F
inst_6 : HasProduct.{w, r, t} (C := D) fun (j : J) ↦ F.obj (f j)
inst_7 : PreservesLimitsOfShape WalkingCospan (forget D (FC := FD) (CC := DD))
inst_8 : PreservesLimit (J := Discrete J) (Discrete.functor fun (b : J) ↦ F.obj (f b)) (forget D (FC := FD) (CC := DD))
x y : ToType (FC := FD) (CC := DD) (F.obj (piObj.{w, v, u} f))
h :
  ∀ (i : J),
    Eq (α := DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) x : DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) y : DD (F.obj (f i)))
⊢ Eq (α := DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
    ((hom (FC := FD) (CC := DD) (Iso.hom (PreservesProduct.iso F f)) :
          (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (j : J) ↦ F.obj (f j)))
        x :
      DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
    ((hom (FC := FD) (CC := DD) (Iso.hom (PreservesProduct.iso F f)) :
          (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (j : J) ↦ F.obj (f j)))
        y :
      DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
have a : ∀ (j : Discrete J),
  Eq (α := DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) j))
    ((hom (FC := FD) (CC := DD) (limit.π (Discrete.functor fun (b : J) ↦ F.obj (f b)) j) :
          (a : DD (limit (Discrete.functor fun (b : J) ↦ F.obj (f b)))) →
            DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj j))
        ((hom (FC := FD) (CC := DD) (piComparison F f) : (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (b : J) ↦ F.obj (f b)))
          x) :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) j))
    ((hom (FC := FD) (CC := DD) (limit.π (Discrete.functor fun (b : J) ↦ F.obj (f b)) j) :
          (a : DD (limit (Discrete.functor fun (b : J) ↦ F.obj (f b)))) →
            DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj j))
        ((hom (FC := FD) (CC := DD) (piComparison F f) : (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (b : J) ↦ F.obj (f b)))
          y) :
      DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) j))
Tactic: apply Concrete.limit_ext _ (piComparison F _ x) (piComparison F _ y)