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

Goal state before:
pp: case h.left
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ {U} ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}

pp: case h.right
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ U = ⋃₀ {U}

Tactic:
· apply subset_trans (singleton_subset_iff.mpr _) (subset_insert _ _)
      use a

Goal state after:
case h.right
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ U = ⋃₀ {U}
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
h :
  ∀ t ∈ s,
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
x✝ : a ∈ ⋃₀ s
s₀ : Set α
hs₀s : s₀ ∈ s
has₀ : a ∈ s₀
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ ⋃₀ s

Tactic:
by
    obtain ⟨b, hbd, hbds₀⟩ := h s₀ hs₀s hd₀ hd₁ hd₂ hd₃ has₀
    exact ⟨b, hbd, Set.subset_sUnion_of_subset s s₀ hbds₀ hs₀s⟩

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := ⋯
U : Set α
⊢ IsOpen[scott α univ] U ↔ IsOpen[upper α] U

Tactic:
rw [@Topology.IsUpper.isTopologicalSpace_basis _ _ (upper α)
    ({ topology_eq_upperTopology := rfl }) U]

Goal state after:
α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := upper α
U : Set α
⊢ IsOpen[scott α univ] U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: case h
L : Type u_1
inst✝ : CompleteLattice L
u v : L
⊢ {x | x (u ⊓ v)} = {x | x u} ∩ {x | x v}

Tactic:
simp_rw [map_inf]

Goal state after:
case h
L : Type u_1
inst✝ : CompleteLattice L
u v : L
⊢ {x | min (x u) (x v)} = {x | x u} ∩ {x | x v}
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
this : IsOpen (⋃ a ∈ c.left, Iio a)
x✝ : α
⊢ x✝ ∈ (fun a ↦ principal a) ⁻¹' Iio c ↔ x✝ ∈ ⋃ a ∈ c.left, Iio a

Tactic:
simp [principal_lt_iff]

Goal state after:
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ hull T (kernel S) ⊆ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}

Tactic:
subset_sInter_iff

Goal state after:
case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ ∀ t' ∈ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}, hull T (kernel S) ⊆ t'
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_1.h₁
x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ BddBelow ((fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = x})

Tactic:
exact ⟨0, by rintro b ⟨⟨u, v⟩, -, rfl⟩; exact hausdorffDist_nonneg⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝ : Nonempty ↑s := Nonempty.to_subtype sne
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ

Tactic:
have : 0 ≤ ε₂ := le_trans (abs_nonneg _) (H ⟨xs, hxs⟩ ⟨xs, hxs⟩)

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝ : Nonempty ↑s := Nonempty.to_subtype sne
this : 0 ≤ ε₂
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: case neg.refine_2.e_s
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
⊢ 0 ∈ ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1)) ∧ ∀ x ∈ ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1)), x = 0

Tactic:
refine ⟨mem_iInter_of_mem fun n => ?_, fun x h => ?_⟩

Goal state after:
case neg.refine_2.e_s.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
n : ℕ
⊢ 0 ∈ range ⇑f ∩ Iio (1 / (↑n + 1))

case neg.refine_2.e_s.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
h✝ : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
x : ℝ
h : x ∈ ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1))
⊢ x = 0
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩

Tactic:
have hpq' : (F p).snd ≍ (F q).snd := (Sigma.mk.inj_iff.1 hpq).2

Goal state after:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
hpq' : (F p).snd ≍ (F q).snd
⊢ (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩
Module: Mathlib.Topology.Sheaves.Points

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
x✝³ x✝² : (grothendieckTopology X).Point
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ x✝¹ = x✝

Tactic:
ext; subsingleton

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case neg
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
p : GHSpace
hp : ¬p ∉ t
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)

Tactic:
rcases hcov _ (Set.not_notMem.1 hp) n with ⟨s, ⟨scard, scover⟩⟩
      rcases Cardinal.lt_aleph0.1 (scard.trans_lt Cardinal.natCast_lt_aleph0) with ⟨N, hN⟩
      rw [hN, Nat.cast_le] at scard
      have : #s = #(Fin N) := by rw [hN, Cardinal.mk_fin]
      obtain ⟨E⟩ := Quotient.exact this
      use s, N, scard, E
      simp only [scover, imp_true_iff]

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
Aq : ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
⊢ ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩)

Tactic:
have hpq' : (F p).snd ≍ (F q).snd := (Sigma.mk.inj_iff.1 hpq).2

Goal state after:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
Aq : ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
hpq' : (F p).snd ≍ (F q).snd
⊢ ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩)
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Injective ⇑(ConcreteCategory.hom (F.stalkToFiber x))

Tactic:
by
  apply TopCat.stalkToFiber_injective
  intro U V fU hU fV hV e
  rcases hU ⟨x, U.2⟩ with ⟨U', mU, iU, gU, wU⟩
  rcases hV ⟨x, V.2⟩ with ⟨V', mV, iV, gV, wV⟩
  have wUx := wU ⟨x, mU⟩
  dsimp at wUx; rw [wUx] at e; clear wUx
  have wVx := wV ⟨x, mV⟩
  dsimp at wVx; rw [wVx] at e; clear wVx
  rcases F.germ_eq x mU mV gU gV e with ⟨W, mW, iU', iV', (e' : F.map iU'.op gU = F.map iV'.op gV)⟩
  use ⟨W ⊓ (U' ⊓ V'), ⟨mW, mU, mV⟩⟩
  refine ⟨?_, ?_, ?_⟩
  · change W ⊓ (U' ⊓ V') ⟶ U.val
    exact Opens.infLERight _ _ ≫ Opens.infLELeft _ _ ≫ iU
  · change W ⊓ (U' ⊓ V') ⟶ V.val
    exact Opens.infLERight _ _ ≫ Opens.infLERight _ _ ≫ iV
  · intro w
    specialize wU ⟨w.1, w.2.2.1⟩
    specialize wV ⟨w.1, w.2.2.2⟩
    refine wU.trans <| .trans ?_ wV.symm
    rw [← F.germ_res iU' w w.2.1, ← F.germ_res iV' w w.2.1,
      CategoryTheory.types_comp_apply, CategoryTheory.types_comp_apply, e']

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
ho : IsOpen[inst✝] s
⊢ IsOpen[constructibleTopology X] s

Tactic:
by
  apply TopologicalSpace.isOpen_generateFrom_of_mem
  simp [constructibleTopologySubbasis, ho, hs]

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact sᶜ
ho : IsClosed[inst✝] s
⊢ IsOpen[constructibleTopology X] s

Tactic:
by
  apply TopologicalSpace.isOpen_generateFrom_of_mem
  simp [constructibleTopologySubbasis, ho, hs]

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✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ∃ᶠ (x : F) in nhdsWithin (↑z) Y, ∃ (h : x ∈ segment ℝ ↑y ↑y'), ⟨x, h⟩ ∈ J
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
hfx : ∀ᶠ (x' : F) in nhdsWithin (↑z) Y, f (↑x) x' < b'
this :
  ∀ᶠ (z' : F) in nhdsWithin (↑z) Y,
    (∃ (hz' : z' ∈ segment ℝ ↑y ↑y'), ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y') →
      ∃ (hz' : z' ∈ segment ℝ ↑y ↑y'),
        x ∈ sublevelLeft X f b' z' ∧ ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
⊢ ∃ z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y', x ∈ sublevelLeft X f b' ↑z'

Tactic:
by
    obtain ⟨z', hz', hxz'1, hxz'2⟩ := hz.mp this |>.exists
    exact ⟨⟨z', hz'⟩, ⟨hxz'2, hxz'1⟩⟩

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

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ (∃ V ∈ 𝓤 X, ball x V ⊆ s) → ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

pp: case mpr
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ (∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 X, ball x V ⊆ s

Tactic:
· rintro ⟨V, V_in, V_sub⟩
    rw [IsUltraUniformity.hasBasis.mem_iff'] at V_in
    obtain ⟨U, ⟨U_in, U_sym, U_trans⟩, U_sub⟩ := V_in
    refine ⟨U, U_in, U_sym, U_trans, (UniformSpace.ball_mono U_sub _).trans V_sub⟩

Goal state after:
case mpr
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ (∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 X, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
left✝¹ : SetRel.IsSymm V
left✝ : SetRel.IsTrans V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 X, ball x V ⊆ s

Tactic:
exact ⟨V, V_in, V_sub⟩

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: case right
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : CompleteLinearOrder β
inst✝¹⁰ : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
hlsc : LowerSemicontinuousOn (fun x ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn (fun y ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn (fun y ↦ ⨅ x ∈ X, f x y) Y b
⊢ IsSaddlePointOn X Y f a b

Tactic:
rw [isSaddlePointOn_iff' ha hb]

Goal state after:
case right
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : CompleteLinearOrder β
inst✝¹⁰ : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
hlsc : LowerSemicontinuousOn (fun x ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn (fun y ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn (fun y ↦ ⨅ x ∈ X, f x y) Y b
⊢ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b