mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι✝ : Sort y
s t u : Set α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Subsingleton ι
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
⊢ borel ((i : ι) → X i) ≤ MeasurableSpace.pi

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
inst✝¹⁵ : TopologicalSpace α✝
inst✝¹⁴ : MeasurableSpace α✝
inst✝¹³ : OpensMeasurableSpace α✝
inst✝¹² : TopologicalSpace β✝
inst✝¹¹ : MeasurableSpace β✝
inst✝¹⁰ : OpensMeasurableSpace β✝
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
inst✝¹⁵ : TopologicalSpace α✝
inst✝¹⁴ : MeasurableSpace α✝
inst✝¹³ : OpensMeasurableSpace α✝
inst✝¹² : TopologicalSpace β✝
inst✝¹¹ : MeasurableSpace β✝
inst✝¹⁰ : OpensMeasurableSpace β✝
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
⊢ SecondCountableTopology β

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iio)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ SecondCountableTopology α

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iic)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝¹ : Preorder α
a b x : α
μ : Measure α
inst✝ : OrderClosedTopology α
⊢ (𝓝[Icc a b] x).IsMeasurablyGenerated

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝¹ : Preorder α
a b x : α
μ : Measure α
inst✝ : R1Space α
⊢ ∀ ⦃s : Set α⦄, s ∈ cocompact α → ∃ t ∈ cocompact α, MeasurableSet t ∧ t ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝² : PartialOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : SecondCountableTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable fun a ↦ f a ≤ g a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : SecondCountableTopology α
inst✝ : OrderClosedTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable fun a ↦ f a < g a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hα : SecondCountableTopology α
F : Set α → Set β := fun a ↦ {y | ∃ b, IsOpen[inst✝⁹] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
⊢ ∀ (a : Set α), IsOpen[inst✝⁹] (F a)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
⊢ MeasurableSet s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
⊢ MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Icc l u = S} ≤ borel α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
d : ℝ≥0∞
⊢ d ≤ infEDist x s ↔ ∀ y ∈ s, d ≤ edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ι : Type u_2
f : ι → Set α
I : Set ι
x : α
⊢ infEDist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, infEDist x (f i)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
⊢ infEDist x s < r ↔ ∃ y ∈ s, edist x y < r

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
⊢ ⨅ z ∈ s, edist y z + edist x y = (⨅ z ∈ s, edist y z) + edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
⊢ infEDist x s ≤ edist x y + infEDist y s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ infEDist x s + ediam s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ 1 ≠ ∞

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ ∀ (x y : α), infEDist x s ≤ infEDist y s + 1 * edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
⊢ 0 < ↑ε / 2

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < ↑ε / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ↑ε / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ↑ε / 2
z : α
zs : z ∈ s
dyz : edist y z < ↑ε / 2
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ↑ε / 2 + ↑ε / 2 =
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ↑ε

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infEDist x s = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : infEDist x s = 0
ε : ℝ≥0∞
εpos : ε > 0
⊢ infEDist x s < ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hα : SecondCountableTopology α
F : Set α → Set β := fun a ↦ {y | ∃ b, IsOpen[inst✝⁹] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst✝⁹] (F a)
⊢ s = ⋃ a ∈ countableBasis α, a ×ˢ F a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ x ∈ s ↔ infEDist x s = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEDist x E ↔ x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) ↔
    x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEDist x E

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
⊢ edist x y ≤ r

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
⊢ Disjoint (closedEBall x r) s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
t : Set α
Φ : α → β
hΦ : Isometry Φ
⊢ infEDist (Φ x) (Φ '' t) = infEDist x t

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
⊢ x ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen[inst✝¹²] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
⊢ ∀ (a : Set β), IsOpen[inst✝¹²] (F a)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ⋃ n, F n ⊆ U

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
⊢ x ∉ Uᶜ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
x✝ : ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
y : α
yx : y ≤ x
hy1 : y ≤ b
hy2 : y ∈ t
hy : x ≤ b
⊢ x < a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEDist x Uᶜ = 0
⊢ 0 < infEDist x Uᶜ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
⊢ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ z ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ x ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ∃ F,
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun y ↦ edist x y

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen[inst✝¹²] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst✝¹²] (F a)
⊢ s = ⋃ a ∈ countableBasis β, F a ×ˢ a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun y ↦ edist x y
y : α
ys : y ∈ s
hy : IsMinOn (fun y ↦ edist x y) s y
⊢ edist x y ≤ infEDist x s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
⊢ ∃ y ∈ s, infEDist x s = edist x y

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : SecondCountableTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
s : Set α
hd : Dense s
⊢ ∀ (x : α), IsBot x → x ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Icc l u = S}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
⊢ MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S} ≤ borel α

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
⊢ OpensMeasurableSpace (α × β)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α' : Type u_6
inst✝¹ : TopologicalSpace α'
inst✝ : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : μ (frontier s) = 0
h' : μ (frontier s') = 0
⊢ frontier s ∩ closure[inst✝¹] s' ∪ closure[inst✝¹] s ∩ frontier s' ⊆ frontier s ∪ frontier s'

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α' : Type u_6
inst✝¹ : TopologicalSpace α'
inst✝ : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : μ (frontier s) = 0
h' : μ (frontier s') = 0
⊢ μ (frontier s) + μ (frontier s') = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α' : Type u_6
inst✝¹ : TopologicalSpace α'
inst✝ : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : μ (frontier s) = 0
h' : μ (frontier s') = 0
⊢ μ (frontier (s ∩ s')) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type u_6
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
inst✝ : T0Space α
x y : α
⊢ (∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) → x = y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ hausdorffEDist s s = 0

Tactic:
by

Goal state after: