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₁ : 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
h₂ :
  Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Cone.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 (x : Discrete (Fin n)) ↦
              match (motive :=
                (x : Discrete (Fin n)) →
                  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                    Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                x with
              | { as := i } => s.π.app { as := i.succ } })
      (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 })
    (NatTrans.app
      (Cone.π
        { pt := s.1,
          π :=
            Discrete.natTrans fun (x : Discrete (Fin n)) ↦
              match (motive :=
                (x : Discrete (Fin n)) →
                  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                    Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                x with
              | { as := i } => s.π.app { as := i.succ } })
      { as := j })
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Cone.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 (x : Discrete (Fin n)) ↦
              match (motive :=
                (x : Discrete (Fin n)) →
                  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                    Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                x with
              | { as := i } => s.π.app { as := i.succ } })
      (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 })
    (NatTrans.app
      (Cone.π
        { pt := s.1,
          π :=
            Discrete.natTrans fun (x : Discrete (Fin n)) ↦
              match (motive :=
                (x : Discrete (Fin n)) →
                  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                    Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                x with
              | { as := i } => s.π.app { as := i.succ } })
      { as := j })

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- 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₁ : 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
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 }) (s.π.app { as := j.succ })
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Cone.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 (x : Discrete (Fin n)) ↦
              match (motive :=
                (x : Discrete (Fin n)) →
                  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                    Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                x with
              | { as := i } => s.π.app { as := i.succ } })
      (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 })
    (NatTrans.app
      (Cone.π
        { pt := s.1,
          π :=
            Discrete.natTrans fun (x : Discrete (Fin n)) ↦
              match (motive :=
                (x : Discrete (Fin n)) →
                  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                    Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                x with
              | { as := i } => s.π.app { as := i.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₁ : 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
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 ≫ (extendFan c₁ c₂).π.app { as := j.succ })
⊢ 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 }) (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₁ : 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
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 ≫
      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)
⊢ 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 ≫ (extendFan c₁ c₂).π.app { as := j.succ })

Tactic:
dsimp only [extendFan_π_app]

Premises used: CategoryTheory.extendFan_π_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₁ : 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
h₂ 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 })
⊢ 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)

Tactic:
rw [Fin.cases_succ]

Premises used: Fin.cases_succ
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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) })
rw : HasLimit.{0, 0, v, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 })
⊢ HasLimit K

Tactic:
rw [← hasLimit_iff_of_iso that]

Premises used: CategoryTheory.Limits.hasLimit_iff_of_iso
-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
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.{0, 0, v, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 })

Tactic:
apply hasProduct_fin

Premises used: _private.0.CategoryTheory.hasProduct_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 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
f : Fin 0 → C
this : PreservesLimitsOfShape (Discrete (Fin 0)) F := ⋯
⊢ PreservesLimit (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 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
n : ℕ
⊢ ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F

Tactic:
haveI := preservesFinOfPreservesBinaryAndTerminal n
-- 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 : 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
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)))))))
⊢ PreservesLimit (Discrete.functor f) F

Tactic:
apply
      preservesLimit_of_preserves_limit_cone
        (extendFanIsLimit f (limit.isLimit _) (limit.isLimit _)) _

Premises used: CategoryTheory.extendFanIsLimit, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- 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 : 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
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))
⊢ 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 (isLimitMapConeFanMkEquiv _ _ _).symm _

Premises used: CategoryTheory.Limits.isLimitMapConeFanMkEquiv, Equiv.symm, DFunLike.coe
-- 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 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
n : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F

Tactic:
⟨fun {K} ↦ ?_⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfShape.mk
-- 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 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
n : ℕ
refine : ∀ {K : Functor.{0, v, 0, u} (Discrete (Fin n)) C}, PreservesLimit K F
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F

Tactic:
refine ⟨fun {K} ↦ ?_⟩
-- 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 : 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 (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⟩
-- 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 : 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) })
this : PreservesLimit (J := Discrete (Fin n)) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) F
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_iso_diagram F that

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram
-- 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
refine_1 : f 0 ⟶ c₂.pt
refine_2 : (i : Fin n) → f i.succ ⟶ c₂.pt
⊢ (b : Fin (n + 1)) → f b ⟶ c₂.pt

Tactic:
refine Fin.cases ?_ ?_
-- 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
⊢ f 0 ⟶ c₂.pt

Tactic:
apply c₂.inl

Premises used: CategoryTheory.Limits.BinaryCofan.inl
-- 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
i : Fin n
⊢ f i.succ ⟶ c₂.pt

Tactic:
apply c₁.ι.app ⟨i⟩ ≫ c₂.inr

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Cocone.ι, CategoryTheory.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)
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 }
⊢ (extendCofan c₁ c₂).pt ⟶ s.pt

Tactic:
apply (BinaryCofan.IsColimit.desc' t₂ (s.ι.app ⟨0⟩) _).1

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.BinaryCofan.IsColimit.desc', OfNat.ofNat, Subtype.val, CategoryTheory.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)
⊢ 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 t₁.desc ⟨_, Discrete.natTrans fun i => s.ι.app ⟨i.as.succ⟩⟩

Premises used: Fin.succ, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Discrete.natTrans, CategoryTheory.Discrete.mk, CategoryTheory.Discrete.as, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.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)
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)) }

Tactic:
Fin.inductionOn j ?_ ?_

Premises used: Fin.inductionOn