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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
this : infEDist x ∅ ≤ hausdorffEDist s ∅
⊢ hausdorffEDist s ∅ = ∞

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
this : infEDist x ∅ ≤ hausdorffEDist s ∅
⊢ hausdorffEDist s ∅ = ∞
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 ∧ Ico l u = S}

Tactic:
simpa using

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hs : s.Nonempty
⊢ IsGLB ((fun x_1 ↦ dist x x_1) '' s) (infDist x s)

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hs : s.Nonempty
⊢ IsGLB ((fun x_1 ↦ dist x x_1) '' s) (⨅ y, dist x ↑y)
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:
simpa using

Goal state after:
α : 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: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E = ⋂ ε ∈ s, cthickening ε E

Tactic:
apply Subset.antisymm

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

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.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:
simpa using

Goal state after:
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hne : s.Nonempty
x : α
⊢ ∃ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, infDist x s = dist x y
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case neg
α : 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

Tactic:
apply Subset.antisymm

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

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.Thickening

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

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ x ∈ E
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
⊢ ∀ x ∈ s, infEDist x t ≤ ENNReal.ofReal r

Tactic:
simpa using

Goal state after:
α : 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
⊢ ∀ x ∈ s, infEDist x t ≤ ENNReal.ofReal r
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
⊢ ∀ x ∈ t, infEDist x s ≤ ENNReal.ofReal r

Tactic:
simpa using

Goal state after:
α : 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
⊢ ∀ x ∈ t, infEDist x s ≤ ENNReal.ofReal r
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
  rw [cthickening_eq_biUnion_closedBall E hδ, hE.closure_eq]

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:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∃ y ∈ range ⇑f, p y) ↔ ∃ x, p (f x)
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:
simpa using

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 y x < r
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist u t ≠ ∞
I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
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 : α
⊢ (s.sup f) a = s.sup fun c ↦ (f c) a

Tactic:
classical
  refine Finset.induction_on s rfl ?_
  intro a s _ ih
  rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]

Goal state after:
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 ∈ (f.restrict s).range
h0 : r ≠ 0
hs : MeasurableSet s
⊢ r ∈ ⇑f '' s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : MeasurableSet s
⊢ ∃ x ∈ s, f x = r
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 g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
⊢ ∀ b ∈ s, IsBot (g b)

Tactic:
simpa using

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 g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
⊢ ∀ b ∈ s, IsBot (g b)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
β : Type u_2
f : α → β
k : α
x : β
x✝ : x ∈ f '' Ici k
y : α
hy : y ∈ Ici k
hfy : f y = x
⊢ (fun x ↦ f (x + k)) (y - k) = x

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
β : Type u_2
f : α → β
k : α
x : β
x✝ : x ∈ f '' Ici k
y : α
hy : y ∈ Ici k
hfy : f y = x
⊢ f y = x
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case pos
α : 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 g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
b : δ
hb : b ∈ s
A : ∀ (i : ι), f' i b = f i b
⊢ IsLUB {a | ∃ i, f' i b = a} (g b)

Tactic:
simpa using

Goal state after:
case pos
α : 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 g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
b : δ
hb : b ∈ s
A : ∀ (i : ι), f' i b = f i b
⊢ IsLUB {a | ∃ i, f i b = a} (g b)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ n, (eapprox f n) a = f a

Tactic:
rw [eapprox, iSup_approx_apply ennrealRatEmbed f a hf rfl]
  refine le_antisymm (iSup_le fun i => iSup_le fun hi => hi) (le_of_not_gt ?_)
  intro h
  rcases ENNReal.lt_iff_exists_rat_btwn.1 h with ⟨q, _, lt_q, q_lt⟩
  have :
    (Real.toNNReal q : ℝ≥0∞) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k := by
    refine le_iSup_of_le (Encodable.encode q) ?_
    rw [ennrealRatEmbed_encode q]
    exact le_iSup_of_le (le_of_lt q_lt) le_rfl
  exact lt_irrefl _ (lt_of_le_of_lt this lt_q)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ n, ⇑(eapprox f n) = f

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (x : α), ⨆ i, (eapprox f i) x = f x
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
x : α
hx : x ∈ s \ {x₀}
⊢ x ≠ x₀

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
x : α
hx : x ∈ s \ {x₀}
⊢ ¬x = x₀
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 : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}
B : ∀ (c : α), MeasurableSet {x | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
⊢ {b | BddAbove (range fun i ↦ f i b)} = {x | ∃ n, ∀ (i : ι), f i x ≤ u n}

Tactic:
apply Subset.antisymm

Goal state after:
case h₁
α : 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 : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}
B : ∀ (c : α), MeasurableSet {x | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
⊢ {b | BddAbove (range fun i ↦ f i b)} ⊆ {x | ∃ n, ∀ (i : ι), f i x ≤ u n}

case h₂
α : 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 : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}
B : ∀ (c : α), MeasurableSet {x | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
⊢ {x | ∃ n, ∀ (i : ι), f i x ≤ u n} ⊆ {b | BddAbove (range fun i ↦ f i b)}
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inl
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : IsEmpty ι
⊢ Measurable fun b ↦ ⨆ i, f i b

Tactic:
simp [iSup_of_empty']

Goal state after:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: case refine_1
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
q : ℚ
h₁ : z < ↑q ∧ x - ε < ↑q
h₂ : ↑q < x
⊢ |↑q - x| < ε

Tactic:
simpa using

Goal state after:
case refine_1
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
q : ℚ
h₁ : z < ↑q ∧ x - ε < ↑q
h₂ : ↑q < x
⊢ x - ε < ↑q
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: case refine_2
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < ↑q
h₂ : ↑q < z ∧ ↑q < x + ε
⊢ |↑q - x| < ε

Tactic:
simpa using

Goal state after:
case refine_2
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < ↑q
h₂ : ↑q < z ∧ ↑q < x + ε
⊢ ↑q < x + ε
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
h : f ≤ g
⊢ f.lintegral μ ≤ g.lintegral μ

Tactic:
refine Monotone.of_left_le_map_sup (f := (lintegral · μ)) (fun f g ↦ ?_) h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ f.lintegral μ ≤ (f ⊔ g).lintegral μ
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : AddZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (f + g).FinMeasSupp μ

Tactic:
add_eq_map₂

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : AddZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p ↦ p.1 + p.2) (f.pair g)).FinMeasSupp μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
F0 : Subtype p → δ → α := fun j x ↦ ⨅ i, f (↑i) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun x ↦ F0 (reparam x j) x
hF1 : F1 = fun x ↦ F0 (reparam x j) x
⊢ Measurable F1

Tactic:
let g : ℕ → Subtype p := Classical.choose (exists_surjective_nat (Subtype p))

Goal state after:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
F0 : Subtype p → δ → α := fun j x ↦ ⨅ i, f (↑i) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun x ↦ F0 (reparam x j) x
hF1 : F1 = fun x ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose ⋯
⊢ Measurable F1
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
h : Measurable fun x ↦ ↑(f x)
⊢ Measurable f

Tactic:
simpa using

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
h : Measurable fun x ↦ ↑(f x)
⊢ Measurable f
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
μ : Measure α
h : AEMeasurable (fun x ↦ ↑(f x)) μ
⊢ AEMeasurable f μ

Tactic:
simpa using

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
μ : Measure α
h : AEMeasurable (fun x ↦ ↑(f x)) μ
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ Measurable fun p ↦ (↑p).toENNReal

Tactic:
simpa using

Goal state after:
⊢ Measurable fun p ↦ ENNReal.ofReal p
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_4
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ ↑r * ⊥

Tactic:
mul_comm _ ⊥

Goal state after:
case refine_4
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ ⊥ * ↑r
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β := fun x ↦ if h : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose else ⋯.some
x : α
hx : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
⊢ Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β := fun x ↦ if h : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose else ⋯.some
x : α
hx : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
⊢ Tendsto (fun n ↦ f n x) L (𝓝 ⋯.choose)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β := fun x ↦ if h : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
x : α
hx : Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))
h_eq : f_lim x = AEMeasurable.mk f_lim hf_lim x
⊢ Tendsto (fun n ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β := fun x ↦ if h : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
x : α
hx : Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))
h_eq : f_lim x = AEMeasurable.mk f_lim hf_lim x
⊢ Tendsto (fun n ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x ↦ 1) μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ (As n).indicator (fun x ↦ 1) x) L (𝓝 (A.indicator (fun x ↦ 1) x))

Tactic:
simpa using

Goal state after:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x ↦ 1) μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
⊢ (nearestPtInd e (N + 1)) x ≤ N + 1

Tactic:
| succ N ihN =>

Goal state after: