awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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)) }
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)) }
⊢ (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)) }

Tactic:
refine Fin.inductionOn j ?_ ?_
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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 := 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:
apply (BinaryCofan.IsColimit.desc' t₂ _ _).2.1

Premises used: And.left, CategoryTheory.Limits.BinaryCofan.IsColimit.desc', Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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
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)) })
⊢ (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:
dsimp only [extendCofan_ι_app]

Premises used: CategoryTheory.extendCofan_ι_app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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
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 })
⊢ 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:
rw [Fin.cases_succ, assoc, (BinaryCofan.IsColimit.desc' t₂ _ _).2.2, t₁.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, And.right, Fin.cases_succ, CategoryTheory.Limits.BinaryCofan.IsColimit.desc', Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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)
    (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:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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 })
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 })
⊢ 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 })

Tactic:
apply BinaryCofan.IsColimit.hom_ext t₂

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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 = s.ι.app { as := 0 }
⊢ 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:
rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.1]

Premises used: And.left, CategoryTheory.Limits.BinaryCofan.IsColimit.desc', Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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 = s.ι.app { as := 0 }

Tactic:
apply w ⟨0⟩

Premises used: CategoryTheory.Discrete.mk, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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₂.inr ≫ m = t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } }
⊢ 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:
rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.2]

Premises used: And.right, CategoryTheory.Limits.BinaryCofan.IsColimit.desc', Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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₂ :
  ∀ (j : Discrete (Fin n)),
    c₁.ι.app j ≫ c₂.inr ≫ m =
      NatTrans.app
        (Cocone.ι { pt := s.1, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } }) j
⊢ c₂.inr ≫ m = t₁.desc { pt := s.pt, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } }

Tactic:
apply t₁.uniq ⟨_, _⟩

Premises used: CategoryTheory.Limits.Cocone.mk, CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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
j : Fin n
h₂ :
  Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) (s.ι.app { as := j.succ })
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : 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.1, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } }))
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m)
    (NatTrans.app
      (Cocone.ι { pt := s.1, ι := Discrete.natTrans fun (i : Discrete (Fin n)) ↦ s.ι.app { as := i.as.succ } })
      { as := j })

Tactic:
dsimp only [Discrete.natTrans_app]

Premises used: CategoryTheory.Discrete.natTrans_app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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
j : Fin n
h₂ :
  Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) ((extendCofan c₁ c₂).ι.app { as := j.succ } ≫ m)
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) (s.ι.app { as := j.succ })

Tactic:
rw [← w ⟨j.succ⟩]

Premises used: Fin.succ, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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
j : Fin n
h₂ :
  Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ f x ⟶ c₂.pt) c₂.inl (fun (i : Fin n) ↦ c₁.ι.app { as := i } ≫ c₂.inr)
        j.succ ≫
      m)
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) ((extendCofan c₁ c₂).ι.app { as := j.succ } ≫ m)

Tactic:
dsimp only [extendCofan_ι_app]

Premises used: CategoryTheory.extendCofan_ι_app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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
j : Fin n
h₂ :
  Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) ((c₁.ι.app { as := j } ≫ c₂.inr) ≫ m)
h₃ h₄ :
  Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m) (c₁.ι.app { as := j } ≫ c₂.inr ≫ m)
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := j : Discrete (Fin n) }) s.1)
    (c₁.ι.app { as := j } ≫ c₂.inr ≫ m)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ f x ⟶ c₂.pt) c₂.inl (fun (i : Fin n) ↦ c₁.ι.app { as := i } ≫ c₂.inr)
        j.succ ≫
      m)

Tactic:
rw [Fin.cases_succ, assoc]

Premises used: CategoryTheory.Category.assoc, Fin.cases_succ
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
n : ℕ
K : Functor.{0, v, 0, u} (Discrete (Fin n)) C
that : K ≅ Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 } :=
  Discrete.natIso fun (x : Discrete (Fin n)) ↦
    match (motive :=
      (x : Discrete (Fin n)) →
        K.obj x ≅ Functor.obj.{0, v, 0, u} (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) x)
      x with
    | { as := as } => Iso.refl (K.obj { as := as })
rw : HasColimit.{0, 0, v, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 })
⊢ HasColimit K

Tactic:
rw [hasColimit_iff_of_iso that]

Premises used: CategoryTheory.Limits.hasColimit_iff_of_iso
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
n : ℕ
K : Functor.{0, v, 0, u} (Discrete (Fin n)) C
that : K ≅ Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 } :=
  Discrete.natIso fun (x : Discrete (Fin n)) ↦
    match (motive :=
      (x : Discrete (Fin n)) →
        K.obj x ≅ Functor.obj.{0, v, 0, u} (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) x)
      x with
    | { as := as } => Iso.refl (K.obj { as := as })
⊢ HasColimit.{0, 0, v, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 })

Tactic:
apply hasCoproduct_fin

Premises used: _private.0.CategoryTheory.hasCoproduct_fin
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteCoproducts.{v, u} C
f : Fin 0 → C
this : PreservesColimitsOfShape (Discrete (Fin 0)) F := ⋯
⊢ PreservesColimit (Discrete.functor f) F

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteCoproducts.{v, u} C
n : ℕ
⊢ ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F

Tactic:
haveI := preserves_fin_of_preserves_binary_and_initial n