awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
I : Finset (Discrete α)
X Y : Functor.{w, v, w, u} (Discrete α) C
x : X ⟶ Y
j : Discrete ↥I
⊢ Eq (α :=
    (piObj.{w, v, u} fun (x : ↥I) ↦ X.obj (↑x : Discrete α)) ⟶
      Functor.obj ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y) j)
    (CategoryStruct.comp (Y := limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
      (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥I) ↦ Y.obj (↑x : Discrete α))
        (Pi.map fun (x_1 : ↥I) ↦ x.app (↑x_1 : Discrete α))
        (Iso.hom
          (HasLimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (Y.obj (↑x.as : Discrete α))))))
      (limit.π ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y) j))
    (CategoryStruct.comp (Y := limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
      (CategoryStruct.comp (Y := limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ X))
        (Iso.hom (HasLimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (X.obj (↑x.as : Discrete α)))))
        (limMap (Functor.whiskerLeft (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) x)))
      (limit.π ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y) j))

Tactic:
simp [Pi.map]

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

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₁ : Fan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryFan.{v, u} (f 0) c₁.pt
⊢ c₂.pt ⟶ f 0

Tactic:
apply c₂.fst

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

Tactic:
apply c₂.snd ≫ c₁.π.app ⟨i⟩

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryFan.snd, 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₁ : 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)
apply :
  Functor.obj.{0, v, 0, u} (C := Discrete (Fin (n + 1))) (Functor.obj (Functor.const (Discrete (Fin (n + 1)))) s.pt)
      { as := 0 : Discrete (Fin (n + 1)) } ⟶
    c₁.pt
⊢ s.pt ⟶ (extendFan c₁ c₂).pt

Tactic:
apply (BinaryFan.IsLimit.lift' t₂ (s.π.app ⟨0⟩) _).1

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryFan.IsLimit.lift', 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₁ : 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)
⊢ Functor.obj.{0, v, 0, u} (C := Discrete (Fin (n + 1))) (Functor.obj (Functor.const (Discrete (Fin (n + 1)))) s.pt)
      { as := 0 : Discrete (Fin (n + 1)) } ⟶
    c₁.pt

Tactic:
apply t₁.lift ⟨_, Discrete.natTrans fun ⟨i⟩ => s.π.app ⟨i.succ⟩⟩

Premises used: CategoryTheory.Limits.Cone.π, Quiver.Hom, Fin.succ, CategoryTheory.Discrete.functor, CategoryTheory.Limits.Cone.pt, CategoryTheory.Discrete.natTrans, CategoryTheory.Discrete.mk, CategoryTheory.extendFanIsLimit.match_2, CategoryTheory.Functor.const, Fin, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Limits.IsLimit.lift, CategoryTheory.Discrete
-- 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)
x : Discrete (Fin (n + 1))
j : Fin (n + 1)
⊢ (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  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 : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      (extendFan c₁ c₂).π.app { as := j } =
    s.π.app { as := j : Discrete (Fin (n + 1)) }

Tactic:
Fin.inductionOn j ?_ ?_

Premises used: Fin.inductionOn
-- 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)
x : Discrete (Fin (n + 1))
j : Fin (n + 1)
⊢ (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  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 : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      (extendFan c₁ c₂).π.app { as := 0 } =
    s.π.app { as := 0 : Discrete (Fin (n + 1)) }

Tactic:
apply (BinaryFan.IsLimit.lift' t₂ _ _).2.1

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift', And.left, 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₁ : 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)
x : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
refine_2 :
  (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  Discrete.natTrans fun (x : Discrete (Fin n)) ↦ s.π.app { as := x.as.succ : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      Fin.cases (motive := fun (x : Fin (n + 1)) ↦ c₂.pt ⟶ f x) c₂.fst (fun (i : Fin n) ↦ c₂.snd ≫ c₁.π.app { as := i })
        i.succ =
    s.π.app { as := i.succ : Discrete (Fin (n + 1)) }
⊢ (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  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 : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      (extendFan c₁ c₂).π.app { as := i.succ } =
    s.π.app { as := i.succ : Discrete (Fin (n + 1)) }

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)
x : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
refine_2 :
  Eq.{v + 1} (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i.succ : Discrete (Fin (n + 1)) })
    (NatTrans.app
        (Cone.π { pt := s.pt, π := Discrete.natTrans fun (x : Discrete (Fin n)) ↦ s.π.app { as := x.as.succ } })
        { as := i } :
      Functor.obj.{0, v, 0, u}
          (Functor.obj (Functor.const (Discrete (Fin n)))
            (Cone.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 (x : Discrete (Fin n)) ↦ s.π.app { as := x.as.succ : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) }))
          { as := i : Discrete (Fin n) } ⟶
        Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) { as := i : Discrete (Fin n) })
    (s.π.app { as := i.succ })
⊢ (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  Discrete.natTrans fun (x : Discrete (Fin n)) ↦ s.π.app { as := x.as.succ : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      Fin.cases (motive := fun (x : Fin (n + 1)) ↦ c₂.pt ⟶ f x) c₂.fst (fun (i : Fin n) ↦ c₂.snd ≫ c₁.π.app { as := i })
        i.succ =
    s.π.app { as := i.succ : Discrete (Fin (n + 1)) }

Tactic:
rw [Fin.cases_succ, ← assoc, (BinaryFan.IsLimit.lift' t₂ _ _).2.2, t₁.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryFan.IsLimit.lift', And.right, Fin.cases_succ, CategoryTheory.Limits.IsLimit.fac, 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₁ : 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)
x : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
⊢ Eq.{v + 1} (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i.succ : Discrete (Fin (n + 1)) })
    (NatTrans.app
        (Cone.π { pt := s.pt, π := Discrete.natTrans fun (x : Discrete (Fin n)) ↦ s.π.app { as := x.as.succ } })
        { as := i } :
      Functor.obj.{0, v, 0, u}
          (Functor.obj (Functor.const (Discrete (Fin n)))
            (Cone.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 (x : Discrete (Fin n)) ↦ s.π.app { as := x.as.succ : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) }))
          { as := i : Discrete (Fin n) } ⟶
        Functor.obj.{0, v, 0, u} (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₁ : 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
h₁ :
  m ≫ c₂.fst =
    (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  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 : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      c₂.fst
h₂ :
  m ≫ c₂.snd =
    (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  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 : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      c₂.snd
⊢ m =
    (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
          (t₁.lift
            { pt := s.pt,
              π :=
                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.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt)

Tactic:
apply BinaryFan.IsLimit.hom_ext t₂

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.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₁ : 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
h₁ : m ≫ c₂.fst = s.π.app { as := 0 }
⊢ m ≫ c₂.fst =
    (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  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 : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      c₂.fst

Tactic:
rw [(BinaryFan.IsLimit.lift' t₂ _ _).2.1]

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift', And.left, 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₁ : 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
⊢ m ≫ c₂.fst = 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₁ : 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
h₂ :
  m ≫ c₂.snd =
    t₁.lift
      { pt := s.pt,
        π :=
          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 } }
⊢ m ≫ c₂.snd =
    (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  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 : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      c₂.snd

Tactic:
rw [(BinaryFan.IsLimit.lift' t₂ _ _).2.2]

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift', And.right, 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₁ : 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
h₂ :
  ∀ (j : Discrete (Fin n)),
    (m ≫ c₂.snd) ≫ c₁.π.app 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 } })
        j
⊢ m ≫ c₂.snd =
    t₁.lift
      { pt := s.pt,
        π :=
          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 } }

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

Premises used: CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Limits.Cone.mk