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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam s = ∞ → ediam (cthickening (↑ε) s) = ∞

pp: case refine_2
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ∞ → ediam (cthickening (↑ε) s) = ∞

pp: case refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (ediam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam s = ∞ → ediam (cthickening (↑ε) s) = ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ∀ (i : Subtype (Membership.mem s)), edist x ↑i ≠ ∞

Tactic:
·

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ∀ (i : Subtype (Membership.mem s)), edist x ↑i ≠ ∞
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ∞ → ediam (cthickening (↑ε) s) = ∞

pp: case refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (ediam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ∞ → ediam (cthickening (↑ε) s) = ∞
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (ediam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε

Tactic:
·

Goal state after:
case refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (ediam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case pos
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

pp: case neg
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
·

Goal state after:
case pos
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

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

Tactic:
·

Goal state after:
case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α ≤ MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Ioc l u = S}
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case neg.inl
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : ¬Bornology.IsBounded s
hε : 0 ≤ 0
⊢ diam (thickening 0 s) ≤ diam s + 2 * 0

pp: case neg.inr
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
·

Goal state after:
case neg.inl
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : ¬Bornology.IsBounded s
hε : 0 ≤ 0
⊢ diam (thickening 0 s) ≤ diam s + 2 * 0
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case neg.inr
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
·

Goal state after:
case neg.inr
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

Tactic:
·

Goal state after:
case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Ioc l u = S} ≤ borel α
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : 0 < ε
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅

pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : ε ≤ 0
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅

Tactic:
·

Goal state after:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : 0 < ε
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : ε ≤ 0
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅

Tactic:
·

Goal state after:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : ε ≤ 0
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
⊢ μ = ν

Tactic:
refine @ext_of_Ico_finite αᵒᵈ _ _ _ _ _ ‹_› μ ν _ hμν fun a b hab => ?_
  erw [Ico_toDual (α := α)]
  exact h hab

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

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ ContinuousAt (fun x ↦ (infDist x ∅)⁻¹) x

pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ ContinuousAt (fun x ↦ (infDist x s)⁻¹) x

Tactic:
·

Goal state after:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ ContinuousAt (fun x ↦ (infDist x ∅)⁻¹) x
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ ContinuousAt (fun x ↦ (infDist x s)⁻¹) x

Tactic:
·

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ ContinuousAt (fun x ↦ (infDist x s)⁻¹) x
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2} ⊆ {S | ∃ l u, l < u ∧ Ico l u = S}

pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ⋃₀ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2} = univ

pp: case refine_3
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}, μ s_1 ≠ ∞

pp: case refine_4
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s

Tactic:
·

Goal state after:
case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2} ⊆ {S | ∃ l u, l < u ∧ Ico l u = S}
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hle : dist z x ≤ dist y x
⊢ False

pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt✝ : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist y x < dist z x
⊢ False

Tactic:
·

Goal state after:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hle : dist z x ≤ dist y x
⊢ False
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt✝ : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist y x < dist z x
⊢ False

Tactic:
·

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt✝ : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist y x < dist z x
⊢ False
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case h₁
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E

pp: case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E

Tactic:
·

Goal state after:
case h₁
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ⋃₀ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2} = univ

pp: case refine_3
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}, μ s_1 ≠ ∞

pp: case refine_4
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s

Tactic:
·

Goal state after:
case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ⋃₀ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2} = univ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E

Tactic:
·

Goal state after:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
ε : ℝ
hε : ε ∈ s
⊢ cthickening δ E ⊆ thickening ε E

pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ i ∈ s, thickening i E ⊆ cthickening δ E

Tactic:
·

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
ε : ℝ
hε : ε ∈ s
⊢ cthickening δ E ⊆ thickening ε E
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_3
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}, μ s_1 ≠ ∞

pp: case refine_4
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s

Tactic:
·

Goal state after:
case refine_3
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}, μ s_1 ≠ ∞
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ i ∈ s, thickening i E ⊆ cthickening δ E

Tactic:
·

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ i ∈ s, thickening i E ⊆ cthickening δ E
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ENNReal.ofReal (max rs rt)

pp: case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)

Tactic:
·

Goal state after:
case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ENNReal.ofReal (max rs rt)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening δ E = ⋂ ε, ⋂ (_ : max 0 δ < ε), thickening ε E

Tactic:
by
  rw [← cthickening_max_zero, cthickening_eq_iInter_thickening]
  exact le_max_left _ _

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

Goal state before:
pp: case pos
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : s ⊆ Ioi 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E

pp: case neg
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E

Tactic:
·

Goal state after:
case pos
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : s ⊆ Ioi 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_4
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s

Tactic:
·

Goal state after:
case refine_4
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)

Tactic:
·

Goal state after:
case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case neg.h₁
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ ⋂ δ ∈ s, cthickening δ E

pp: case neg.h₂
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ ⋂ δ ∈ s, cthickening δ E ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
·

Goal state after:
case neg.h₁
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ ⋂ δ ∈ s, cthickening δ E
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case neg.h₂
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ ⋂ δ ∈ s, cthickening δ E ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
·

Goal state after:
case neg.h₂
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ ⋂ δ ∈ s, cthickening δ E ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : s = ∅
⊢ hausdorffDist s ∅ = 0

pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : s.Nonempty
⊢ hausdorffDist s ∅ = 0

Tactic:
·

Goal state after:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : s = ∅
⊢ hausdorffDist s ∅ = 0