awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
Goal:
J : Type v
inst : Category.{w, v} J
inst_1 : IsCofiltered.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set (↑(F.obj j) : Type (max u v)))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set (↑(F.obj i) : Type (max u v))), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat :
  ∀ (i j : J) (f : i ⟶ j) (V : Set (↑(F.obj j) : Type (max u v))) (_hV : V ∈ T j),
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
              (F.map f)) :
          (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
        V ∈
      T i
U0 : Set (↑C.pt : Type (max u v))
U : (i : J) → Set (↑(F.obj i) : Type (max u v))
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 :
  U0 =
    ⋂ i ∈ G,
      (fun (x : (↑C.pt : Type (max u v))) ↦
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (C.π.app i) :
              (a : (↑(((Functor.const J).obj C.pt).obj i) : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
            x) ⁻¹'
        U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty.{w + 1} (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun (x : J) (he : x ∈ G) ↦ ⋯.some
Vs : J → Set (↑(F.obj j) : Type (max u v)) :=
  fun (e : J) ↦
    if h : e ∈ G then
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (F.map (g e h))) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj e) : Type (max u v))) ⁻¹'
        U e
    else Set.univ
V : Set (↑(F.obj j) : Type (max u v)) := ⋂ e ∈ G, Vs e
h :
  Eq (α := Set (↑C.pt : Type (max u v)))
    (⋂ i ∈ G,
      (fun (x : (↑C.pt : Type (max u v))) ↦
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (C.π.app i) :
              (a : (↑(((Functor.const J).obj C.pt).obj i) : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
            x) ⁻¹'
        U i)
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            carrier) (C.π.app j)) :
        (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
      V)
⊢ U0 =
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (C.π.app j)) :
        (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
      V

Tactic:
rw [h2]
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
Goal:
J : Type v
inst : Category.{w, v} J
inst_1 : IsCofiltered.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set (↑(F.obj j) : Type (max u v)))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set (↑(F.obj i) : Type (max u v))), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat :
  ∀ (i j : J) (f : i ⟶ j) (V : Set (↑(F.obj j) : Type (max u v))) (_hV : V ∈ T j),
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
              (F.map f)) :
          (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
        V ∈
      T i
U0 : Set (↑C.pt : Type (max u v))
U : (i : J) → Set (↑(F.obj i) : Type (max u v))
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 :
  U0 =
    ⋂ i ∈ G,
      (fun (x : (↑C.pt : Type (max u v))) ↦
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (C.π.app i) :
              (a : (↑(((Functor.const J).obj C.pt).obj i) : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
            x) ⁻¹'
        U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty.{w + 1} (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun (x : J) (he : x ∈ G) ↦ ⋯.some
Vs : J → Set (↑(F.obj j) : Type (max u v)) :=
  fun (e : J) ↦
    if h : e ∈ G then
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (F.map (g e h))) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj e) : Type (max u v))) ⁻¹'
        U e
    else Set.univ
V : Set (↑(F.obj j) : Type (max u v)) := ⋂ e ∈ G, Vs e
e : J
h :
  ∀ (he : e ∈ G),
    Eq (α := Set (↑C.pt : Type (max u v)))
      ((fun (x : (↑C.pt : Type (max u v))) ↦
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (C.π.app e) :
              (a : (↑(((Functor.const J).obj C.pt).obj e) : Type (max u v))) → (↑(F.obj e) : Type (max u v)))
            x) ⁻¹'
        U e)
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (C.π.app j)) :
          (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
        Vs e)
⊢ Eq (α := e ∈ G → Set (↑C.pt : Type (max u v)))
    (fun (x : e ∈ G) ↦
      (fun (x : (↑C.pt : Type (max u v))) ↦
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (C.π.app e) :
              (a : (↑(((Functor.const J).obj C.pt).obj e) : Type (max u v))) → (↑(F.obj e) : Type (max u v)))
            x) ⁻¹'
        U e)
    fun (i : e ∈ G) ↦
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (C.π.app j)) :
        (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
      Vs e

Tactic:
ext1 he
-- Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered
Goal:
J : Type v
inst : Category.{w, v} J
inst_1 : IsCofiltered.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set (↑(F.obj j) : Type (max u v)))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set (↑(F.obj i) : Type (max u v))), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat :
  ∀ (i j : J) (f : i ⟶ j) (V : Set (↑(F.obj j) : Type (max u v))) (_hV : V ∈ T j),
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
              (F.map f)) :
          (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
        V ∈
      T i
U0 : Set (↑C.pt : Type (max u v))
U : (i : J) → Set (↑(F.obj i) : Type (max u v))
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 :
  U0 =
    ⋂ i ∈ G,
      (fun (x : (↑C.pt : Type (max u v))) ↦
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (C.π.app i) :
              (a : (↑(((Functor.const J).obj C.pt).obj i) : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
            x) ⁻¹'
        U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty.{w + 1} (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun (x : J) (he : x ∈ G) ↦ ⋯.some
Vs : J → Set (↑(F.obj j) : Type (max u v)) :=
  fun (e : J) ↦
    if h : e ∈ G then
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (F.map (g e h))) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj e) : Type (max u v))) ⁻¹'
        U e
    else Set.univ
V : Set (↑(F.obj j) : Type (max u v)) := ⋂ e ∈ G, Vs e
e : J
he : e ∈ G
⊢ Eq (α := Set (↑C.pt : Type (max u v)))
    ((fun (x : (↑C.pt : Type (max u v))) ↦
        (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (C.π.app e) :
            (a : (↑(((Functor.const J).obj C.pt).obj e) : Type (max u v))) → (↑(F.obj e) : Type (max u v)))
          x) ⁻¹'
      U e)
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            carrier) (C.π.app j)) :
        (a : (↑(((Functor.const J).obj C.pt).obj j) : Type (max u v))) → (↑(F.obj j) : Type (max u v))) ⁻¹'
      Vs e)

Tactic:
simp [Vs, dif_pos he, ← Set.preimage_comp, ← coe_comp]

Premises used: dif_pos, Set.preimage_comp, TopCat.coe_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty.{v + 1} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
inl : IsEmpty J → (partialSections F H).Nonempty
inr : Nonempty J → (partialSections F H).Nonempty
⊢ (partialSections F H).Nonempty

Tactic:
cases isEmpty_or_nonempty J

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty.{v + 1} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h_1 : IsEmpty J
⊢ (partialSections F H).Nonempty

Tactic:
⟨isEmptyElim, fun {j} => IsEmpty.elim' inferInstance j.1⟩

Premises used: isEmptyElim, inferInstance, Set.Nonempty, IsEmpty.elim', Exists.intro, PSigma.fst
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty.{v + 1} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h_1 : IsEmpty J
⊢ (partialSections F H).Nonempty

Tactic:
exact ⟨isEmptyElim, fun {j} => IsEmpty.elim' inferInstance j.1⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty.{v + 1} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h_1 : Nonempty J
⊢ IsCofiltered J

Tactic:
haveI : IsCofiltered J := ⟨⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty.{v + 1} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h_1 : Nonempty J
this : IsCofiltered J
h₁ :
  (fun (j : J) ↦
      if hj : j ∈ G then
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
              F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hj)) :
            (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj j) : Type v))
          (Nonempty.some ⋯)
      else ⋯.some) ∈
    partialSections F H
⊢ (partialSections F H).Nonempty

Tactic:
use fun j : J =>
    if hj : j ∈ G then F.map (IsCofiltered.infTo G H hj) (h (IsCofiltered.inf G H)).some
    else (h _).some

Premises used: CategoryTheory.IsCofiltered.inf, CategoryTheory.ConcreteCategory.hom, Membership.mem, Nonempty.some, CategoryTheory.Functor.map, dite, CategoryTheory.IsCofiltered.infTo, DFunLike.coe
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
obtain :
  ∀ (u : (j : J) → (↑(F.obj j) : Type (max u v)))
    (hu :
      Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
        (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
        u),
    Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
⊢ Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))

Tactic:
obtain ⟨u, hu⟩ :=
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed (fun G => partialSections F _)
      (partialSections.directed F) (fun G => partialSections.nonempty F _)
      (fun G => IsClosed.isCompact (partialSections.closed F _)) fun G =>
      partialSections.closed F _

Premises used: IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, TopCat.partialSections, IsClosed.isCompact, TopCat.partialSections.closed, Sigma.snd, TopCat.partialSections.directed, TopCat.partialSections.nonempty
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
u : (j : J) → (↑(F.obj j) : Type (max u v))
hu :
  Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
    (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u
property :
  Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max v u))))
    {u : (j : J) → (↑(F.obj j) : Type (max v u)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC :=
                carrier) (F.map f) :
              (a : (↑(F.obj i) : Type (max v u))) → (↑(F.obj j) : Type (max v u)))
            (u i) =
          u j}
    u
⊢ Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))

Tactic:
use u
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
u : (j : J) → (↑(F.obj j) : Type (max u v))
hu :
  Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
    (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u
X Y : J
f : X ⟶ Y
⊢ Membership.mem (γ := Finset J) {X, Y} X

Tactic:
grind
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
u : (j : J) → (↑(F.obj j) : Type (max u v))
hu :
  Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
    (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u
X Y : J
f : X ⟶ Y
⊢ Membership.mem (γ := Finset J) {X, Y} Y

Tactic:
grind
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
u : (j : J) → (↑(F.obj j) : Type (max u v))
hu :
  Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
    (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u
X Y : J
f : X ⟶ Y
G : FiniteDiagram J :=
  Sigma.mk (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) {X, Y}
    {PSigma.mk (β := fun (X_1 : J) ↦
        (Y_1 : J) ×'
          (_ : Membership.mem (γ := Finset J) {X, Y} X_1) ×'
            (_ : Membership.mem (γ := Finset J) {X, Y} Y_1) ×' (X_1 ⟶ Y_1))
        X
        (PSigma.mk (β := fun (Y_1 : J) ↦
          (_ : Membership.mem (γ := Finset J) {X, Y} X) ×' (_ : Membership.mem (γ := Finset J) {X, Y} Y_1) ×' (X ⟶ Y_1))
          Y
          (PSigma.mk (β := fun (x : Membership.mem (γ := Finset J) {X, Y} X) ↦
            (_ : Membership.mem (γ := Finset J) {X, Y} Y) ×' (X ⟶ Y)) ⋯
            (PSigma.mk (β := fun (x : Membership.mem (γ := Finset J) {X, Y} Y) ↦ X ⟶ Y) ⋯ f)))}
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
          (F.map f) :
        (a : (↑(F.obj X) : Type (max v u))) → (↑(F.obj Y) : Type (max v u)))
      (u X) =
    u Y

Tactic:
hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)

Premises used: Finset.mem_singleton_self, Exists.intro, rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
u : (j : J) → (↑(F.obj j) : Type (max u v))
hu :
  Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
    (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u
X Y : J
f : X ⟶ Y
G : FiniteDiagram J :=
  Sigma.mk (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) {X, Y}
    {PSigma.mk (β := fun (X_1 : J) ↦
        (Y_1 : J) ×'
          (_ : Membership.mem (γ := Finset J) {X, Y} X_1) ×'
            (_ : Membership.mem (γ := Finset J) {X, Y} Y_1) ×' (X_1 ⟶ Y_1))
        X
        (PSigma.mk (β := fun (Y_1 : J) ↦
          (_ : Membership.mem (γ := Finset J) {X, Y} X) ×' (_ : Membership.mem (γ := Finset J) {X, Y} Y_1) ×' (X ⟶ Y_1))
          Y
          (PSigma.mk (β := fun (x : Membership.mem (γ := Finset J) {X, Y} X) ↦
            (_ : Membership.mem (γ := Finset J) {X, Y} Y) ×' (X ⟶ Y)) ⋯
            (PSigma.mk (β := fun (x : Membership.mem (γ := Finset J) {X, Y} Y) ↦ X ⟶ Y) ⋯ f)))}
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
          (F.map f) :
        (a : (↑(F.obj X) : Type (max v u))) → (↑(F.obj Y) : Type (max v u)))
      (u X) =
    u Y

Tactic:
exact hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)

Premises used: Finset.mem_singleton_self, Exists.intro, rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
ι : Type v
α : ι → TopCat
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan.{v, u} α).pt
h : ∀ (j : Discrete ι), m ≫ (piFan.{v, u} α).π.app j = S.π.app j
w :
  ∀ (x : (↑S.pt : Type (max u v))),
    Eq (α := (↑(piFan.{v, u} α).pt : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) m :
            (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
          x :
        (↑(piFan.{v, u} α).pt : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (X := S.pt) (Y := (piFan.{v, u} α).pt)
              (ofHom
                {
                  toFun := fun (s : (↑S.1 : Type (max u v))) (i : ι) ↦
                    (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                          (CC := carrier) (X :=
                          Functor.obj (Functor.obj (Functor.const (Discrete ι)) S.pt) { as := i : Discrete ι })
                          (S.π.app { as := i }) :
                        (a : (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := i }) : Type (max u v))) →
                          (↑((Discrete.functor α).obj { as := i }) : Type (max u v)))
                      s,
                  continuous_toFun := ⋯ }) :
            (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
          x :
        (↑(piFan.{v, u} α).pt : Type (max u v)))
⊢ m =
    ofHom
      {
        toFun := fun (s : (↑S.1 : Type (max u v))) (i : ι) ↦
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (X := Functor.obj (Functor.obj (Functor.const (Discrete ι)) S.pt) { as := i : Discrete ι })
                (S.π.app { as := i }) :
              (a : (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := i }) : Type (max u v))) →
                (↑((Discrete.functor α).obj { as := i }) : Type (max u v)))
            s,
        continuous_toFun := ⋯ }

Tactic:
ext x
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
ι : Type v
α : ι → TopCat
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan.{v, u} α).pt
h : ∀ (j : Discrete ι), m ≫ (piFan.{v, u} α).π.app j = S.π.app j
x : (↑S.pt : Type (max u v))
w :
  ∀ (i : ι),
    Eq (α := (↑(α i) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) m :
            (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
          x i :
        (↑(α i) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (X := S.pt) (Y := (piFan.{v, u} α).pt)
              (ofHom
                {
                  toFun := fun (s : (↑S.1 : Type (max u v))) (i : ι) ↦
                    (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                          (CC := carrier) (X :=
                          Functor.obj (Functor.obj (Functor.const (Discrete ι)) S.pt) { as := i : Discrete ι })
                          (S.π.app { as := i }) :
                        (a : (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := i }) : Type (max u v))) →
                          (↑((Discrete.functor α).obj { as := i }) : Type (max u v)))
                      s,
                  continuous_toFun := ⋯ }) :
            (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
          x i :
        (↑(α i) : Type (max u v)))
⊢ Eq (α := (↑(piFan.{v, u} α).pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            m :
          (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
        x :
      (↑(piFan.{v, u} α).pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (X := S.pt) (Y := (piFan.{v, u} α).pt)
            (ofHom
              {
                toFun := fun (s : (↑S.1 : Type (max u v))) (i : ι) ↦
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                        (CC := carrier) (X :=
                        Functor.obj (Functor.obj (Functor.const (Discrete ι)) S.pt) { as := i : Discrete ι })
                        (S.π.app { as := i }) :
                      (a : (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := i }) : Type (max u v))) →
                        (↑((Discrete.functor α).obj { as := i }) : Type (max u v)))
                    s,
                continuous_toFun := ⋯ }) :
          (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
        x :
      (↑(piFan.{v, u} α).pt : Type (max u v)))

Tactic:
funext i