awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryFan.{v, u} (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone.{0, v, 0, u} (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
j : Fin n
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C) s.1
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }))
    (m ≫ c₂.snd ≫ c₁.π.app { as := j })
    (m ≫
      Fin.cases (motive := fun (x : Fin (n + 1)) ↦ c₂.pt ⟶ f x) c₂.fst (fun (i : Fin n) ↦ c₂.snd ≫ c₁.π.app { as := i })
        j.succ)
have h₂ : Eq (α :=
  Quiver.Hom.{v, u} (V := C) s.1
    (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }))
  (m ≫ c₂.snd ≫ c₁.π.app { as := j }) (m ≫ c₂.snd ≫ c₁.π.app { as := j })
Tactic: rw [Fin.cases_succ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
inst_2 : HasTerminal.{v, u} C
n : ℕ
K : Functor.{0, v, 0, u} (Discrete (Fin n)) C
that : (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun (x : Discrete (Fin n)) ↦
    match (motive :=
      (x : Discrete (Fin n)) →
        Functor.obj.{0, v, 0, u} (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) x ≅ K.obj x)
      x with
    | { as := as } =>
      Iso.refl
        (Functor.obj.{0, v, 0, u} (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 })
          { as := as : Discrete (Fin n) })
⊢ HasLimit K
have rw : HasLimit.{0, 0, v, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 })
Tactic: rw [← hasLimit_iff_of_iso that]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
n : ℕ
⊢ ∀ (f : Fin (n + 1) → C), PreservesLimit (Discrete.functor f) F
have this : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
Tactic: haveI := preservesFinOfPreservesBinaryAndTerminal n
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
n : ℕ
this : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ PreservesLimit (Discrete.functor f) F
have f₁ : IsLimit (J := Discrete (Fin (n + 1))) (F := Discrete.functor f ⋙ F)
  (F.mapCone
    (extendFan (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))
      (limit.cone
        (pair (f 0)
          (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
            (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
Tactic: apply
      preservesLimit_of_preserves_limit_cone
        (extendFanIsLimit f (limit.isLimit _) (limit.isLimit _)) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
n : ℕ
this : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ IsLimit (J := Discrete (Fin (n + 1))) (F := Discrete.functor f ⋙ F)
    (F.mapCone
      (extendFan (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))
        (limit.cone
          (pair (f 0)
            (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
have apply : IsLimit.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F := Discrete.functor fun (j : Fin (n + 1)) ↦ F.obj (f j))
  (Fan.mk
    (F.obj
      (Cone.pt.{0, v, 0, u} (F :=
        pair (f 0)
          (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
            (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
        (limit.cone
          (pair (f 0)
            (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
    fun (j : Fin (n + 1)) ↦
    F.map
      (Fin.cases (motive := fun (x : Fin (n + 1)) ↦
        Cone.pt.{0, v, 0, u} (F :=
            pair (f 0)
              (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
            (limit.cone
              (pair (f 0)
                (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                  (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))) ⟶
          f x)
        (BinaryFan.fst
          (limit.cone
            (pair (f 0)
              (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
        (fun (i : Fin n) ↦
          BinaryFan.snd
              (limit.cone
                (pair (f 0)
                  (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                    (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))) ≫
            NatTrans.app (Cone.π (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))) { as := i })
        j))
Tactic: apply (isLimitMapConeFanMkEquiv _ _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
n : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F
have refine : ∀ {K : Functor.{0, v, 0, u} (Discrete (Fin n)) C}, PreservesLimit K F
Tactic: refine ⟨fun {K} ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
n : ℕ
K : Functor.{0, v, 0, u} (Discrete (Fin n)) C
that : (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun (x : Discrete (Fin n)) ↦
    match (motive :=
      (x : Discrete (Fin n)) →
        Functor.obj.{0, v, 0, u} (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) x ≅ K.obj x)
      x with
    | { as := i } =>
      Iso.refl
        (Functor.obj.{0, v, 0, u} (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 })
          { as := i : Discrete (Fin n) })
⊢ PreservesLimit K F
have this : PreservesLimit (J := Discrete (Fin n)) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) F
Tactic: haveI := preservesFinOfPreservesBinaryAndTerminal F n fun n => K.obj ⟨n⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
⊢ (b : Fin (n + 1)) → f b ⟶ c₂.pt
have refine_1 : f 0 ⟶ c₂.pt
Tactic: refine Fin.cases ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
refine_1 : f 0 ⟶ c₂.pt
⊢ (b : Fin (n + 1)) → f b ⟶ c₂.pt
have refine_2 : (i : Fin n) → f i.succ ⟶ c₂.pt
Tactic: refine Fin.cases ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
⊢ (extendCofan c₁ c₂).pt ⟶ s.pt
have apply : c₁.pt ⟶
  Functor.obj.{0, v, 0, u} (C := Discrete (Fin (n + 1))) (Functor.obj (Functor.const (Discrete (Fin (n + 1)))) s.pt)
    { as := 0 }
Tactic: apply (BinaryCofan.IsColimit.desc' t₂ (s.ι.app ⟨0⟩) _).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
j : Fin (n + 1)
⊢ (extendCofan c₁ c₂).ι.app { as := j } ≫
      (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.desc
              { pt := s.pt,
                ι :=
                  Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
                Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }) =
    s.ι.app { as := j : Discrete (Fin (n + 1)) }
have refine_1 : (extendCofan c₁ c₂).ι.app { as := 0 } ≫
    (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (t₁.desc
            { pt := s.pt,
              ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
              Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
      c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }) =
  s.ι.app { as := 0 : Discrete (Fin (n + 1)) }
Tactic: refine Fin.inductionOn j ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
j : Fin (n + 1)
refine_1 :
  (extendCofan c₁ c₂).ι.app { as := 0 } ≫
      (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.desc
              { pt := s.pt,
                ι :=
                  Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
                Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }) =
    s.ι.app { as := 0 : Discrete (Fin (n + 1)) }
⊢ (extendCofan c₁ c₂).ι.app { as := j } ≫
      (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.desc
              { pt := s.pt,
                ι :=
                  Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
                Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }) =
    s.ι.app { as := j : Discrete (Fin (n + 1)) }
have refine_2 : ∀ (i : Fin n),
  (extendCofan c₁ c₂).ι.app { as := i.castSucc } ≫
        (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 : Discrete (Fin (n + 1)) })
              (t₁.desc
                { pt := s.pt,
                  ι :=
                    Discrete.natTrans fun (i : Discrete (Fin n)) ↦
                      s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
                  Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C)
                    (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
          c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }) =
      s.ι.app { as := i.castSucc : Discrete (Fin (n + 1)) } →
    (extendCofan c₁ c₂).ι.app { as := i.succ } ≫
        (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 : Discrete (Fin (n + 1)) })
              (t₁.desc
                { pt := s.pt,
                  ι :=
                    Discrete.natTrans fun (i : Discrete (Fin n)) ↦
                      s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
                  Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C)
                    (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
          c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }) =
      s.ι.app { as := i.succ : Discrete (Fin (n + 1)) }
Tactic: refine Fin.inductionOn j ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ (extendCofan c₁ c₂).ι.app { as := i.succ } ≫
      (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.desc
              { pt := s.pt,
                ι :=
                  Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
                Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }) =
    s.ι.app { as := i.succ : Discrete (Fin (n + 1)) }
have refine_2 : Eq.{v + 1} (α := Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i.succ : Discrete (Fin (n + 1)) } ⟶ s.pt)
  (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ f x ⟶ c₂.pt) c₂.inl (fun (i : Fin n) ↦ c₁.ι.app { as := i } ≫ c₂.inr)
        i.succ ≫
      (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.desc
              { pt := s.pt,
                ι :=
                  Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
                Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }) :
    Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i.succ : Discrete (Fin (n + 1)) } ⟶ s.pt)
  (s.ι.app { as := i.succ } :
    Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i.succ : Discrete (Fin (n + 1)) } ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin (n + 1)))) s.pt)
        { as := i.succ : Discrete (Fin (n + 1)) })
Tactic: dsimp only [extendCofan_ι_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ Eq.{v + 1} (α := Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i.succ : Discrete (Fin (n + 1)) } ⟶ s.pt)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ f x ⟶ c₂.pt) c₂.inl (fun (i : Fin n) ↦ c₁.ι.app { as := i } ≫ c₂.inr)
          i.succ ≫
        (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 : Discrete (Fin (n + 1)) })
              (t₁.desc
                { pt := s.pt,
                  ι :=
                    Discrete.natTrans fun (i : Discrete (Fin n)) ↦
                      s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
                  Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C)
                    (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
          c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 }) :
      Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i.succ : Discrete (Fin (n + 1)) } ⟶ s.pt)
    (s.ι.app { as := i.succ } :
      Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i.succ : Discrete (Fin (n + 1)) } ⟶
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin (n + 1)))) s.pt)
          { as := i.succ : Discrete (Fin (n + 1)) })
have refine_2 : Eq.{v + 1} (α := Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i.succ : Discrete (Fin (n + 1)) } ⟶ s.pt)
  (NatTrans.app
      (Cocone.ι { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })
      { as := i } :
    Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := i : Discrete (Fin n) } ⟶
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete (Fin n)))
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
            { pt := s.pt,
              ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ : Discrete (Fin (n + 1)) } :
              Cocone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) }))
        { as := i : Discrete (Fin n) })
  (s.ι.app { as := i.succ })
Tactic: rw [Fin.cases_succ, assoc, (BinaryCofan.IsColimit.desc' t₂ _ _).2.2, t₁.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ m =
    (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })) :
      c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 })
have h₁ : c₂.inl ≫ m =
  c₂.inl ≫
    (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })) :
      c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 })
Tactic: apply BinaryCofan.IsColimit.hom_ext t₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
h₁ :
  c₂.inl ≫ m =
    c₂.inl ≫
      (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
            (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })) :
        c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 })
⊢ m =
    (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })) :
      c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 })
have h₂ : c₂.inr ≫ m =
  c₂.inr ≫
    (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })) :
      c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 })
Tactic: apply BinaryCofan.IsColimit.hom_ext t₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ c₂.inl ≫ m =
    c₂.inl ≫
      (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
            (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })) :
        c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 })
have h₁ : c₂.inl ≫ m = s.ι.app { as := 0 }
Tactic: rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.1]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (goal)
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone.{0, v, 0, u} (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ c₂.inr ≫ m =
    c₂.inr ≫
      (↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
            (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })) :
        c₂.pt ⟶ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 })
have h₂ : c₂.inr ≫ m = t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } }
Tactic: rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.2]