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

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

Tactic:
]

Goal state after:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ ∅, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x ∅ ≤ r
⊢ 0 ≤ r
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inr.inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
r : ℝ
hr : 0 ≤ r
hs : s.Nonempty
H1 : ∀ x ∈ s, infDist x ∅ ≤ r
H2 : ∀ x ∈ ∅, infDist x s ≤ r
⊢ 0 ≤ r

Tactic:
]

Goal state after:
case inr.inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
r : ℝ
hr : 0 ≤ r
hs : s.Nonempty
H1 : ∀ x ∈ s, infDist x ∅ ≤ r
H2 : ∀ x ∈ ∅, infDist x s ≤ r
⊢ 0 ≤ r
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 : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ

Tactic:
]

Goal state after:
α : 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 : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ
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✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) ≠ ∞

Tactic:
]

Goal state after:
case refine_1
α : 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)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) ≠ ∞
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✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) = ν (⇑OrderDual.ofDual ⁻¹' Ioc b a)

Tactic:
]

Goal state after:
case refine_2
α : 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)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) = ν (⇑OrderDual.ofDual ⁻¹' Ioc b a)
Module: Mathlib.Topology.MetricSpace.Thickening

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

Tactic:
]

Goal state after:
case inr
δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) =
    ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ
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 ≤ δ
⊢ ⋃ x ∈ E, closedBall x δ = ⋃ x ∈ E, closedBall x δ

Tactic:
]

Goal state after:
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 α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ ν (Iic b) - ν (Iic a) = ν (Iic b) - ν (Iic a)

pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ ν (Iic a) ≠ ∞

pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic a) ≠ ∞

Tactic:
]

Goal state after:
case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ ν (Iic a) ≠ ∞

case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic a) ≠ ∞
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 α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic a) ≠ ∞

Tactic:
]

Goal state after:
case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic a) ≠ ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffEDist s t < ENNReal.ofReal r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r
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
this : hausdorffEDist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y ∈ t, dist x y < r
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEDist s t ≠ ∞
⊢ ∃ x ∈ s, dist x y < r
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEDist t s ≠ ∞
⊢ ∃ x ∈ s, dist x y < r
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}
this : {a | r a (f a)} = ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}
⊢ MeasurableSet (⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b})

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (f a)} = ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}
⊢ MeasurableSet (⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b})
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist t s ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist t s ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
μ : Measure α
⊢ μ univ = μ univ

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist t s ≠ ∞
h : ¬hausdorffEDist s u = ∞
⊢ ¬hausdorffEDist t u = ∞

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist t s ≠ ∞
h : ¬hausdorffEDist s u = ∞
⊢ ¬hausdorffEDist t u = ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist u t ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
Module: Mathlib.Topology.MetricSpace.Thickening

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

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ (edist x y).toReal = (edist x y).toReal

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
ε δ : ℝ
⊢ thickening ε (thickening δ {x}) ⊆ thickening (ε + δ) {x}

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
ε δ : ℝ
⊢ thickening ε (thickening δ {x}) ⊆ thickening (ε + δ) {x}
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
⊢ (∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ thickening i s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
⊢ (∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ thickening i s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: β : Type u_2
δ : Type u_4
inst✝⁶ : TopologicalSpace β
mβ : MeasurableSpace β
inst✝⁵ : BorelSpace β
mδ : MeasurableSpace δ
inst✝⁴ : CompleteLinearOrder β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous fun x_1 ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
this : (⨆ i, f i) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x}
⊢ MeasurableSet (⋃ j ∈ J, {x | c < f j x})

Tactic:
]

Goal state after:
β : Type u_2
δ : Type u_4
inst✝⁶ : TopologicalSpace β
mβ : MeasurableSpace β
inst✝⁵ : BorelSpace β
mδ : MeasurableSpace δ
inst✝⁴ : CompleteLinearOrder β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous fun x_1 ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
this : (⨆ i, f i) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x}
⊢ MeasurableSet (⋃ j ∈ J, {x | c < f j x})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
⊢ Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), cthickening δ s)))

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
⊢ Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), cthickening δ s)))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
A :
  Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[>] 0)
    (𝓝 (μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
a✝ : ℝ
hr : a✝ ∈ Iic 0
⊢ μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) =
    μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ⇑(f.pair g) ⁻¹' {b} ×ˢ {c} = ⇑f ⁻¹' {b} ∩ ⇑g ⁻¹' {c}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ⇑(f.pair g) ⁻¹' {b} ×ˢ {c} = ⇑f ⁻¹' {b} ∩ ⇑g ⁻¹' {c}
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
s t : Set α
hs : IsCompact s
⊢ (∃ i, 0 < i ∧ thickening i s ⊆ t) ↔ ∃ ε > 0, thickening ε s ⊆ t

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
⊢ ⋂ δ, ⋂ (_ : 0 < δ), thickening δ s ⊆ s

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
⊢ ⋂ δ, ⋂ (_ : 0 < δ), thickening δ s ⊆ s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (thickening R s) ≠ ∞
⊢ Tendsto (fun r ↦ μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), thickening δ s)))

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (thickening R s) ≠ ∞
⊢ Tendsto (fun r ↦ μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), thickening δ s)))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s✝ : Finset γ
a✝¹ : α
a : γ
s : Finset γ
a✝ : a ∉ s
ih : (s.sup f) a✝¹ = s.sup fun c ↦ (f c) a✝¹
⊢ ((f a) a✝¹ ⊔ s.sup fun c ↦ (f c) a✝¹) = (f a) a✝¹ ⊔ s.sup fun c ↦ (f c) a✝¹

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ ⇑(piecewise s hs f 0) = s.indicator ⇑f

Tactic:
coe_piecewise,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ s.piecewise ⇑f ⇑0 = s.indicator ⇑f
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ s.indicator ⇑f = s.indicator ⇑f

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.fst '' C) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
]

Goal state after:
case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.fst '' C) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.snd '' D) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
]

Goal state after:
case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.snd '' D) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (⋃ i, s ×ˢ t i)

Tactic:
]

Goal state after:
case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (⋃ i, s ×ˢ t i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (⋃ i, t i ×ˢ s)

Tactic:
]

Goal state after:
case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (⋃ i, t i ×ˢ s)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
⊢ r = 0 ∧ s ≠ univ ∨ r ∈ ⇑f '' s ↔ r = 0 ∧ s ≠ univ ∨ r ∈ ⇑f '' s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun i ↦ f i b) (g b)
⊢ Measurable g

Tactic:
]

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun i ↦ f i b) (g b)
⊢ Measurable g
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ SimpleFunc.range 0
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ SimpleFunc.range 0
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)

Tactic:
]

Goal state after:
case a
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst✝¹
hD : generateFrom D = inst✝
h2C : IsCountablySpanning C
h2D : IsCountablySpanning D
⊢ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D) = generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ ((Finset.range n).sup fun c ↦ ((const α (i c)).restrict {a | i c ≤ f a}) a) =
    (Finset.range n).sup fun k ↦ if i k ≤ f a then i k else 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ ((Finset.range n).sup fun c ↦ ((const α (i c)).restrict {a | i c ≤ f a}) a) =
    (Finset.range n).sup fun k ↦ if i k ≤ f a then i k else 0
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case hunion
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆ U

Tactic:
]

Goal state after:
case hunion
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆ U