mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝ : TopologicalSpace E
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
b : β
y : ↑Y
⊢ IsClosed (sublevelLeft X f b ↑y)

Tactic:
by
  specialize hfy y.val y.prop
  rw [← lowerSemicontinuous_restrict_iff, lowerSemicontinuous_iff_isClosed_preimage] at hfy
  exact hfy b

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ x ∈ s ∧ IsClopen s) id

Tactic:
by
  refine (nhds_basis_uniformity' (IsUltraUniformity.hasBasis)).to_hasBasis' ?_ ?_
  · intro V ⟨hV, h_symm, h_trans⟩
    exact ⟨ball x V, ⟨mem_ball_self _ hV,
      isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity _ hV⟩, le_rfl⟩
  · rintro u ⟨hx, hu⟩
    simp [hu.right.mem_nhds_iff, hx]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Uniformizable

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
h : ∃ u, u.toTopologicalSpace = t
⊢ CompletelyRegularSpace X

Tactic:
obtain ⟨u, rfl⟩ := h

Goal state after:
X : Type u_1
u : UniformSpace X
⊢ CompletelyRegularSpace X