awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
this : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
f₁ :
  IsColimit (J := Discrete (Fin (n + 1))) (F := Discrete.functor f ⋙ F)
    (F.mapCocone
      (extendCofan (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))
        (colimit.cocone
          (pair (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
⊢ PreservesColimit (Discrete.functor f) F

Tactic:
apply
      preservesColimit_of_preserves_colimit_cocone
        (extendCofanIsColimit f (colimit.isColimit _) (colimit.isColimit _)) _

Premises used: CategoryTheory.extendCofanIsColimit, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- 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 : ℕ
this : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
apply :
  IsColimit.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F := Discrete.functor fun (j : Fin (n + 1)) ↦ F.obj (f j))
    (Cofan.mk
      (F.obj
        (Cocone.pt.{0, v, 0, u} (F :=
          pair (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
          (colimit.cocone
            (pair (f 0)
              (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
      fun (j : Fin (n + 1)) ↦
      F.map
        (Fin.cases (motive := fun (x : Fin (n + 1)) ↦
          f x ⟶
            Cocone.pt.{0, v, 0, u} (F :=
              pair (f 0)
                (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                  (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
              (colimit.cocone
                (pair (f 0)
                  (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                    (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
          (BinaryCofan.inl
            (colimit.cocone
              (pair (f 0)
                (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                  (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
          (fun (i : Fin n) ↦
            NatTrans.app (Cocone.ι (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))) { as := i } ≫
              BinaryCofan.inr
                (colimit.cocone
                  (pair (f 0)
                    (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                      (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
          j))
⊢ IsColimit (J := Discrete (Fin (n + 1))) (F := Discrete.functor f ⋙ F)
    (F.mapCocone
      (extendCofan (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))
        (colimit.cocone
          (pair (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))

Tactic:
apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _

Premises used: CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv, 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 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteCoproducts.{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) })
⊢ PreservesColimit (J := Discrete (Fin n)) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) F

Tactic:
haveI := preserves_fin_of_preserves_binary_and_initial 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 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteCoproducts.{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 : PreservesColimit (J := Discrete (Fin n)) (Discrete.functor fun (n_1 : Fin n) ↦ K.obj { as := n_1 }) F
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_iso_diagram F that

Premises used: CategoryTheory.Limits.preservesColimit_of_iso_diagram
-- 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
J : Type u_1
inst_5 : Finite J
⊢ PreservesColimitsOfShape.{u_1, u_1, v, v', u, u'} (Discrete J) F

Tactic:
let ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
  have := preservesShape_fin_of_preserves_binary_and_initial F n
  preservesColimitsOfShape_of_equiv (Discrete.equivalence e).symm _

Premises used: CategoryTheory.preservesShape_fin_of_preserves_binary_and_initial, _private.0.CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initial.match_1, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, Finite.exists_equiv_fin, CategoryTheory.Limits.PreservesColimitsOfShape, CategoryTheory.Equivalence.symm, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
dsimp : 𝟙 i.pt ≫ i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
⊢ Functor.map (Functor.obj (Functor.const J) i.pt) f ≫ i.ι ≫ c₁.π.app { as := j₂ } =
    (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
rw : i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f
rw₁ : i.ι ≫ c₁.π.app { as := j₂ } = i.ι ≫ c₁.π.app { as := j₁ : Discrete J } ≫ F.map f
rw₂ :
  Eq (α := i.pt ⟶ F.obj j₂) (i.ι ≫ c₁.π.app { as := j₂ })
    (i.ι ≫ s ≫ c₂.π.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f })
rw₃ :
  Eq (α := i.pt ⟶ F.obj j₂) (i.ι ≫ c₁.π.app { as := j₂ })
    (i.ι ≫ t ≫ c₂.π.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f })
rw₄ rw₅ :
  Eq (α := i.pt ⟶ F.obj j₂) (i.ι ≫ c₁.π.app { as := j₂ })
    (i.ι ≫
      c₁.π.app
        {
          as :=
            (Sigma.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f)).2 })
⊢ 𝟙 i.pt ≫ i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ : Discrete J }) ≫ F.map f

Tactic:
rw [Category.id_comp, Category.assoc, ← hs ⟨⟨_, _⟩, f⟩, i.condition_assoc, ht]

Premises used: CategoryTheory.Category.assoc, Prod.mk, Sigma.mk, CategoryTheory.Limits.Fork.condition_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
refine_1 : q.1 ⟶ c₁.pt
refine_2 :
  Eq (α := q.1 ⟶ c₂.pt) (t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ s : q.1 ⟶ c₂.pt)
    (t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ t : q.1 ⟶ c₂.pt)
⊢ q.pt ⟶ (buildLimit s t hs ht i).pt

Tactic:
refine hi.lift (Fork.ofι ?_ ?_)

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
refine_1 : (j : J) → q.1 ⟶ F.obj j
⊢ q.1 ⟶ c₁.pt

Tactic:
refine t₁.lift (Fan.mk _ fun j => ?_)

Premises used: CategoryTheory.Limits.Fan.mk, CategoryTheory.Limits.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
j : J
⊢ q.1 ⟶ F.obj j

Tactic:
apply q.π.app j

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
refine_2 :
  ∀ (j : Discrete ((p : J × J) × (p.1 ⟶ p.2))),
    Eq (α :=
      Quiver.Hom.{v, u} (V := C) q.1
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) j))
      ((t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ s) ≫ c₂.π.app j :
        Quiver.Hom.{v, u} (V := C) q.1
          (Functor.obj.{w, v, w, u}
            (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
            j))
      ((t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ t) ≫ c₂.π.app j :
        Quiver.Hom.{v, u} (V := C) q.1
          (Functor.obj.{w, v, w, u}
            (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
            j))
⊢ Eq (α := q.1 ⟶ c₂.pt) (t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ s : q.1 ⟶ c₂.pt)
    (t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ t : q.1 ⟶ c₂.pt)

Tactic:
apply t₂.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
j : (p : J × J) × (p.1 ⟶ p.2)
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C) q.1
      (Functor.obj.{w, v, w, u}
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
        { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) }))
    ((t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ s) ≫ c₂.π.app { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } :
      Quiver.Hom.{v, u} (V := C) q.1
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) }))
    ((t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ t) ≫ c₂.π.app { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } :
      Quiver.Hom.{v, u} (V := C) q.1
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) }))

Tactic:
simp [hs, ht]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s_1 t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s_1 ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s_1 t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
s : Cone F
j : J
⊢ hi.lift
        (Fork.ofι (P := s.1)
          (t₁.lift (Fan.mk s.1 fun (j : J) ↦ s.π.app j) :
            Cone.pt.{w, v, w, u} (J := Discrete J) (F := Discrete.functor F.obj) (Fan.mk s.1 fun (j : J) ↦ s.π.app j) ⟶
              c₁.pt)
          ⋯) ≫
      (buildLimit s_1 t hs ht i).π.app j =
    s.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
m : q.pt ⟶ (buildLimit s t hs ht i).pt
w : ∀ (j : J), m ≫ (buildLimit s t hs ht i).π.app j = q.π.app j
j : Discrete J
⊢ (m ≫ i.ι) ≫ c₁.π.app j =
    (hi.lift
          (Fork.ofι (P := q.1)
            (t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) :
              Cone.pt.{w, v, w, u} (J := Discrete J) (F := Discrete.functor F.obj)
                  (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ⟶
                c₁.pt)
            ⋯) ≫
        i.ι) ≫
      c₁.π.app j

Tactic:
simpa using w j.1

Premises used: CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
inst_2 : HasLimit.{w, w, v, u} (Discrete.functor F.obj)
inst_3 :
  HasLimit.{w, w, v, u} (J := Discrete ((p : J × J) × (p.1 ⟶ p.2))) (C := C)
    (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
inst_4 : HasEqualizers.{v, u} C
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq.{v + 1} (α :=
      Cone.pt.{w, v, w, u} (F := Discrete.functor F.obj) (limit.cone (Discrete.functor F.obj)) ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (CategoryStruct.comp (Y :=
          Cone.pt.{w, v, w, u} (J := Discrete ((p : J × J) × (p.1 ⟶ p.2))) (F :=
            Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
            (limit.cone
              (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)))
          (Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            limit.π (Discrete.functor F.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
              F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)))
          (NatTrans.app
            (Cone.π
              (limit.cone
                (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
                  F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)))
            { as := f }) :
        Cone.pt.{w, v, w, u} (F := Discrete.functor F.obj) (limit.cone (Discrete.functor F.obj)) ⟶
          Functor.obj.{w, v, w, u}
            (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
            { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (NatTrans.app (Cone.π (limit.cone (Discrete.functor F.obj)))
            { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
          F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) :
        Functor.obj.{w, v, w, u}
            (Functor.obj (Functor.const (Discrete J))
              (Cone.pt.{w, v, w, u} (F := Discrete.functor F.obj) (limit.cone (Discrete.functor F.obj))))
            { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ⟶
          F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)

Tactic:
simp