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 → β
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : b < max (f a ↑y) (f a ↑y')
⊢ Disjoint (sublevelLeft X f b ↑y) (sublevelLeft X f b ↑y')

Tactic:
rw [Set.disjoint_iff]

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : b < max (f a ↑y) (f a ↑y')
⊢ sublevelLeft X f b ↑y ∩ sublevelLeft X f b ↑y' ⊆ ∅
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 → β
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : b < max (f a ↑y) (f a ↑y')
⊢ Disjoint (sublevelLeft X f b ↑y) (sublevelLeft X f b ↑y')

Tactic:
by
  rw [Set.disjoint_iff]
  rintro ⟨x, hx⟩ ⟨hx1, hx2⟩
  apply hb.not_ge
  grw [ha x hx]
  simpa using ⟨hx1, hx2⟩

Goal state after:
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✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hfx' : Convex ℝ {x_1 | x_1 ∈ Y ∧ min (f ↑x ↑y) (f ↑x ↑y') ≤ (fun y ↦ f (↑x) y) x_1}
hx : x ∈ sublevelLeft X f b ↑z
⊢ min (f ↑x ↑y) (f ↑x ↑y') ≤ b

Tactic:
rw [convex_iff_segment_subset] at hfx'

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝² : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hfx' :
  ∀ ⦃x_1 : F⦄,
    x_1 ∈ {x_2 | x_2 ∈ Y ∧ min (f ↑x ↑y) (f ↑x ↑y') ≤ (fun y ↦ f (↑x) y) x_2} →
      ∀ ⦃y_1 : F⦄,
        y_1 ∈ {x_2 | x_2 ∈ Y ∧ min (f ↑x ↑y) (f ↑x ↑y') ≤ (fun y ↦ f (↑x) y) x_2} →
          segment ℝ x_1 y_1 ⊆ {x_2 | x_2 ∈ Y ∧ min (f ↑x ↑y) (f ↑x ↑y') ≤ (fun y ↦ f (↑x) y) x_2}
hx : x ∈ sublevelLeft X f b ↑z
⊢ min (f ↑x ↑y) (f ↑x ↑y') ≤ b
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t

Tactic:
apply (hs ht).imp

Goal state after:
case refine_1.f
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ t ∈ {s | IsOpen[inst✝²] s ∧ IsCompact s} → IsOpen[inst✝²] t

case refine_1.g
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ t ∈ {s | IsClosed[inst✝²] s ∧ IsCompact sᶜ} → IsClosed[inst✝²] t
Module: Mathlib.Topology.UniformSpace.Dini

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e ↦ ‖F e x - f x‖) atTop (𝓝 0)
n : ι
hn : ‖F n x - f x‖ < ε
⊢ Continuous[inst✝⁴, _] fun y ↦ ‖F n y - f y‖

Tactic:
by fun_prop

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

Goal state before:
pp: case h_symm
X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ ∀ (i : SetRel X X),
    i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)

Tactic:
exact fun _ ⟨_, hU, _⟩ ↦ by rw [id_eq]; infer_instance

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: case a.inl.mpr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
sup_inf : β
cY : Convex ℝ ∅
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) ∅
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ ∅ fun y ↦ f x y
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
t : β
⊢ t = sup_inf → ∃ x ∈ X, sup_y x = t

Tactic:
· rintro rfl
      exact ⟨_, ne_X.choose_spec, hsup_y _ ne_X.choose_spec⟩

Goal state after: