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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ infDist x s < r ↔ ∃ y ∈ s, dist x y < r

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
⊢ infDist x s ≤ infDist y s + dist 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 ∧ Ioc l u = S}

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
⊢ dist x y ≤ infDist x s + diam s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : 0 < ε
⊢ s = ∅ → thickening ε s = ∅

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : 0 < ε
⊢ (thickening ε s).Nonempty ↔ s.Nonempty

Tactic:
by

Goal state after:
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 → μ (Ico a b) = ν (Ico a b)
⊢ μ = ν

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infDist x s = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infDist x s = 0

Tactic:
by
  rw [← infDist_closure]
  exact infDist_zero_of_mem hx

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
⊢ (thickening ε s).Nonempty ↔ 0 < ε ∧ s.Nonempty

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ x ∉ s ↔ 0 < infDist x s

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ ↑(r / 2) + ↑(r / 2) = ↑r

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
⊢ ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ infDist x (s ∩ closedBall x (dist y x)) = infDist x s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : IsCompact s
hne : s.Nonempty
x y : α
hys : y ∈ s
hy : infEDist x s = edist x y
⊢ infDist x s = dist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hne : s.Nonempty
x : α
⊢ ∃ y ∈ s, infDist x s = dist x y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hne : s.Nonempty
x : α
⊢ ∃ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, infDist x s = dist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
⊢ 0 ≤ hausdorffDist s t

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
⊢ μ = ν

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ, ⋂ (_ : 0 < δ), cthickening δ E

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ hausdorffEDist s t ≤ ENNReal.ofReal (max rs rt)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
⊢ hausdorffEDist s t ≠ ∞

Tactic:
by

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

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

Tactic:
exact cthickening_eq_iInter_thickening rfl.ge E

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ, ⋂ (_ : 0 < δ), thickening δ E

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist s t = hausdorffDist t s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ E

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
⊢ cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ'

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ hausdorffEDist s t ≤ ENNReal.ofReal r

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
⊢ hausdorffDist s t ≤ r

Tactic:
by

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

Goal state before:
pp: δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ

Tactic:
by

Goal state after:
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 α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
⊢ μ = ν

Tactic:
by

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

Goal state before:
pp: δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hE : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ infEDist x s ≤ infEDist x (cthickening δ s) + ENNReal.ofReal δ

Tactic:
by

Goal state after:
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 : ∀ (a : α), μ (Iic a) = ν (Iic a)
⊢ μ = ν

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
⊢ hausdorffDist s t ≤ r

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ infEDist x (cthickening ?m.15 s) + ENNReal.ofReal ?m.15 ≤ infEDist x (thickening δ s) + ENNReal.ofReal δ

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
hs : s.Nonempty
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∀ y ∈ f.range, p y) ↔ ∀ (x : α), p (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∃ y ∈ f.range, p y) ↔ ∃ x, p (f x)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: β : Type u_2
α : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty α
b : β
⊢ ↑(const α b).range = ↑{b}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: β : Type u_2
α : Type u_5
inst✝ : MeasurableSpace α
b : β
⊢ ↑(const α b).range ⊆ ↑{b}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
⊢ ∃ c, ∀ (x : α), f x = c

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
⊢ ∃ y ∈ t, dist x y < r

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
this : r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i
⊢ a ∈ {a | r a (f a)} ↔ a ∈ ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
⊢ {a | r a (f a)} = ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
⊢ ∃ x ∈ s, dist x y < r

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
⊢ MeasurableSet {a | r a (f a)}

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
⊢ infDist x t ≤ infDist x s + hausdorffDist s t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
μ : Measure α
⊢ ∑ y ∈ f.range, μ (⇑f ⁻¹' {y}) = μ univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet sᶜ
f g : α →ₛ β
⊢ ⇑(piecewise sᶜ hs f g) = ⇑(piecewise s ⋯ g f)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
by

Goal state after:
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 α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
⊢ μ = ν

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ ⇑(piecewise univ ⋯ f g) = ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ ⇑(piecewise ∅ ⋯ f g) = ⇑g

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 ↦ Max.max (f a) (g a)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ piecewise s hs f f = f

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 ↦ Min.min (f a) (g a)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist t u ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist s (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : β
⊢ MeasurableSet ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) ⁻¹' {x})

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) t = hausdorffDist s t

Tactic:
by

Goal state after: