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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E

Tactic:
obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEDist_of_notMem_closure h
  filter_upwards [eventually_lt_nhds ε_pos] with δ hδ
  simp only [thickening, mem_ofPred_eq, not_lt]
  exact (ENNReal.ofReal_le_ofReal hδ.le).trans ε_lt.le

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

Goal state before:
pp: X : Type u
inst✝ : PseudoMetricSpace X
x : X
E : Set X
hx : x ∈ E
δ : ℝ
⊢ ball x δ ⊆ thickening δ {x}

Tactic:
simp

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

Goal state before:
pp: case inl
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
h : Bornology.IsBounded ∅
⊢ Bornology.IsBounded (thickening δ ∅)

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ

Tactic:
exact ENNReal.ofReal_le_ofReal h'

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

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

Tactic:
simp

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

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

Tactic:
· simp [hε, thickening_of_nonpos hε]

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 : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal (↑r / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal (↑r / 2)
⊢ z ∈ ⊥

Tactic:
← NNReal.coe_two,

Goal state after:
α : 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 : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal (↑r / ↑2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal (↑r / ↑2)
⊢ z ∈ ⊥
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

Tactic:
exact subset_iInter₂ fun _ hε => cthickening_mono (le_of_lt (hsδ hε)) E

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
⊢ cthickening 0 E = ⋂ δ ∈ s, thickening δ E

Tactic:
apply cthickening_eq_iInter_thickening' le_rfl _ hs₀ hs

Goal state after:
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) ≠ ∞

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:
exacts [hμ hab, h hab]

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:
simp

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:
simp

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:
simp

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:
simp

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 α
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)
a : α
⊢ (fun a ↦ (g (f a)) a) a ∈ ⋃ i ∈ range ⇑f, range ⇑(g i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
a✝ : α
⊢ (f.bind (const α)) a✝ = f a✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Nonempty α
inst✝ : One β
x : β
⊢ x ∈ SimpleFunc.range 1 ↔ x ∈ {1}

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ s

Tactic:
closure_eq_iInter_thickening

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
a✝ : β
⊢ a✝ ∈ f.range ↔ a✝ ∈ ∅

Tactic:
simp

Goal state after:
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)
    (𝓝 (μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))

Tactic:
closure_eq_iInter_thickening

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

Goal state before:
pp: α : 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
⊢ ∅ ∈ 𝓝ˢ ∅

Tactic:
simp

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

Goal state before:
pp: α : 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
⊢ thickening 1 (f '' ∅) ⊆ U

Tactic:
simp

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 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
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
⊢ g = s.piecewise (fun _y ↦ g x) g'

Tactic:
ext b

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
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
b : δ
⊢ g b = s.piecewise (fun _y ↦ g x) g' b
Module: Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst✝ : NullSingletonClass μ
⊢ ∀ i ∈ s, μ {i} = 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass

Goal state before:
pp: X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NullSingletonClass μ
E : Set X
inst✝ : SeparableSpace ↑E
hE : 0 < μ E
⊢ ∃ x, AccPt x (𝓟 E)

Tactic:
by_contra! h
  have : DiscreteTopology E := discreteTopology_of_noAccPts fun x _ => h x
  exact hE.ne' <| (Set.countable_coe_iff.mp <| separableSpace_iff_countable.mp ‹_›).measure_zero μ

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : LinearOrder α
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
a : α
h : b ≤ b + a
⊢ b + a < b + c ↔ b + a < b ∨ ∃ d < c, b + a = b + d

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : LinearOrder α
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
a : α
h : b ≤ b + a
⊢ b + a ≤ b + c ↔ b + a < b ∨ ∃ d ≤ c, b + a = b + d

Tactic:
simp

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

Goal state before:
pp: α : 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
x : α
hx : x ∈ K
this✝ : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
this : V ∈ 𝓝 x
⊢ K ∩ interior V ⊆ interior V

Tactic:
simp

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 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'
⊢ Measurable g

Tactic:
classical
  rcases isEmpty_or_nonempty ι with hι | ⟨⟨i⟩⟩
  · rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩
    · convert! g'_meas
      rwa [compl_empty, eqOn_univ] at hg'
    · have A : ∀ b ∈ s, IsBot (g b) := by simpa using hg
      have B : ∀ b ∈ s, g b = g x := by
        intro b hb
        apply le_antisymm (A b hb (g x)) (A x hx (g b))
      have : g = s.piecewise (fun _y ↦ g x) g' := by
        ext b
        by_cases hb : b ∈ s
        · simp [hb, B]
        · simp [hb, hg' hb]
      rw [this]
      exact Measurable.piecewise hs measurable_const g'_meas
  · have : Nonempty ι := ⟨i⟩
    let f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
    suffices ∀ b, IsLUB { a | ∃ i, f' i b = a } (g b) from
      Measurable.isLUB (fun i ↦ Measurable.piecewise hs (hf i) g'_meas) this
    intro b
    by_cases hb : b ∈ s
    · have A : ∀ i, f' i b = f i b := fun i ↦ by simp [f', hb]
      simpa [A] using hg b hb
    · have A : ∀ i, f' i b = g' b := fun i ↦ by simp [f', hb]
      simp [A, hg' hb, isLUB_singleton]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + ∑ x ∈ (f.pair g).range, x.2 * μ (⇑(f.pair g) ⁻¹' {x}) =
    (map Prod.fst (f.pair g)).lintegral μ + (map Prod.snd (f.pair g)).lintegral μ

Tactic:
by
      rw [map_lintegral, map_lintegral]

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

Goal state before:
pp: q : ℚ
⊢ ↑q + 1 ≠ ↑q + 2

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : (fun x ↦ if q then a else b) =ᶠ[L] fun i ↦ if p i then a else b
hq : q
⊢ map (fun x ↦ a) L ≤ 𝓟 {a}

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
ha✝ : 0 ∈ f.range
ha : 0 ≠ ∞
⊢ 0 * μ (⇑f ⁻¹' {0}) < ∞

Tactic:
simp

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

Goal state before:
pp: a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
b : ℚ
x✝ : b ∈ Rat.cast ⁻¹' Iio a
⊢ Iio ↑b ∈ ⋃ a, {Iio ↑a}

Tactic:
simp

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

Goal state before:
pp: a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
b : ℚ
x✝ : b ∈ Rat.cast ⁻¹' Ioi a
⊢ Ioi ↑b ∈ ⋃ a, {Ioi ↑a}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
n : ℕ
⊢ Ioo (-(↑n + 1)) (↑n + 1) = Ioo ↑(-↑(n + 1)) ↑(↑n + 1)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
⊢ Measurable fun r ↦ (∞, ↑r).1 - (∞, ↑r).2

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
⊢ Measurable fun r ↦ (↑r, ∞).1 - (↑r, ∞).2

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : EReal → α
h : Measurable fun p ↦ f ↑p
⊢ {⊥, ⊤}.Finite

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ Measurable fun x ↦ 0 * x

Tactic:
simp

Goal state after:
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 [f_lim, hx] using hx.choose_spec

Goal state after:
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 [tendsto_indicator_const_apply_iff_eventually] using h_lim

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

Goal state before:
pp: case e_c
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (x ∈ ⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x}) = ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
⊢ (nearestPtInd e 0) x ≤ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
f✝ : β → α
inst✝² : Zero α
inst✝¹ : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
⊢ MeasurableSet ∅ ∧ ∅ ⊆ ∅ ∧ ∀ x ∈ ∅, dist (f x) (0 x) < ε

Tactic:
simp

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

Goal state before:
pp: α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞)
⊢ μ (s ∩ f ⁻¹' Ioo 0 ∞) = ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
rw [← measure_iUnion,
      ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow (ENNReal.one_lt_coe_iff.2 ht) ENNReal.coe_ne_top,
      preimage_iUnion, inter_iUnion]

Goal state after:
case hn
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞)
⊢ Pairwise (Function.onFun Disjoint fun n ↦ s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

case h
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞)
⊢ ∀ (i : ℤ), MeasurableSet (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1)))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ ∫⁻ (x : α), 0 ∂μ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ (⨅ x, f x) * μ univ = ∫⁻ (y : α), ⨅ x, f x ∂μ

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (y : α), ⨆ x, f x ∂μ = (⨆ x, f x) * μ univ

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (⨅ x ∈ s, f x) * μ s = ∫⁻ (y : α) in s, ⨅ x ∈ s, f x ∂μ

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (y : α) in s, ⨆ x ∈ s, f x ∂μ = (⨆ x ∈ s, f x) * μ s

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
by
  rw [lintegral_congr_ae]
  rw [EventuallyEq]
  rwa [ae_restrict_iff' hs]

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
G : Type u_6
inst✝⁴ : Group G
inst✝³ : MulAction G β
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousInv G
inst✝ : ContinuousSMul G β
c : α → G
hc : AEStronglyMeasurable c μ
h : AEStronglyMeasurable (fun x ↦ c x • f x) μ
⊢ (fun i ↦ (c i)⁻¹ • c i • f i) =ᵐ[μ] f

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Monotone fun n ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ⨆ n, ∫⁻ (x : α), f n x ∂μ

Tactic:
rw [← lintegral_iSup' hf h_mono]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Monotone fun n ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨆ n, f n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
⊢ ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
by
  simpa only [lintegral_zero, zero_add] using
    lintegral_add_mul_meas_add_le_le_lintegral (ae_of_all _ fun x => zero_le) hf ε

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case intro.inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
val✝ : Encodable β
h✝ : IsEmpty β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
simp

Goal state after: