mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ c ≤ ‖(hf.approx n) x‖

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ c ≤ ‖(hf.approx n) x‖
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
g : α → β
left✝ : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
Hg : AEStronglyMeasurable g μ
x : α
hx : Tendsto (fun n ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
h'x : g x = AEStronglyMeasurable.mk g Hg x
⊢ Tendsto (fun n ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
g : α → β
left✝ : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
Hg : AEStronglyMeasurable g μ
x : α
hx : Tendsto (fun n ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
h'x : g x = AEStronglyMeasurable.mk g Hg x
⊢ Tendsto (fun n ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ NullMeasurableSet {x | f' x ≤ g x} (μ.restrict s)

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ NullMeasurableSet {x | f' x ≤ g x} (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᵐ[μ] f'
⊢ range ((f' ⁻¹' s).piecewise f' fun x ↦ h_nonempty.some) ⊆ s

Tactic:
]

Goal state after:
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᵐ[μ] f'
⊢ range ((f' ⁻¹' s).piecewise f' fun x ↦ h_nonempty.some) ⊆ s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
n : ℕ
⊢ ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}) ≤
    ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | (SimpleFunc.map c rs) a ≤ f n a})

Tactic:
]

Goal state after:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
n : ℕ
⊢ ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}) ≤
    ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | (SimpleFunc.map c rs) a ≤ f n a})
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ (a : α), f a = g a
⊢ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
by
  simp only [h]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
h : s =ᵐ[μ] t
⊢ ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

Tactic:
]

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
⊢ ∫⁻ (a : α) in s, ?m.31 a ∂μ = ∫⁻ (x : α) in s, g x ∂μ

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ f =ᵐ[μ.restrict s] ?m.31

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

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ f =ᵐ[μ.restrict s] g
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 : α) ∂μ.restrict s, f x = g x

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x = g x
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 : α) ∂μ, x ∈ s → f x = g x

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : Tendsto u atTop (𝓝 0)
x : α
⊢ 0 < f x ↔ ∃ i, x ∈ {x | u i ≤ f x}

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : Tendsto u atTop (𝓝 0)
x : α
⊢ 0 < f x ↔ ∃ i, x ∈ {x | u i ≤ f x}
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
n : ℕ
x : α
hxt : x ∉ t
⊢ (S n ∩ t).indicator (⇑(f_approx n)) x = 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
n : ℕ
x : α
hxt : x ∉ t
⊢ (S n ∩ t).indicator (⇑(f_approx n)) x = 0
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ≤ ε
x : α
⊢ 0 < f x ↔ ∃ i, x ∈ {x | u i ≤ f x}

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ≤ ε
x : α
⊢ 0 < f x ↔ ∃ i, x ∈ {x | u i ≤ f x}
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ,
    x ∈ sᶜ → s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ,
    x ∈ sᶜ → s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
x : α
hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
hx_mem : x ∉ s
⊢ s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
x : α
hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
hx_mem : x ∉ s
⊢ s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ μ (S n ∩ t ∩ ⇑(f_approx n) ⁻¹' {y}) < ∞

pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ y ≠ 0

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ μ (S n ∩ t ∩ ⇑(f_approx n) ⁻¹' {y}) < ∞

case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ y ≠ 0
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
have h_ae_seq_mono : Monotone (aeSeq hf p) := by
    intro n m hnm x
    by_cases hx : x ∈ aeSeqSet hf p
    · exact aeSeq.prop_of_mem_aeSeqSet hf hx hnm
    · simp only [aeSeq, hx, if_false, le_rfl]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ n, aeSeq hf p n) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ n, aeSeq hf p n) a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : Tendsto u atTop (𝓝 0)
u_union : {x | f x ≠ 0} = ⋃ n, {x | u n ≤ f x}
res : μ {x | f x ≠ 0} = 0
⊢ f =ᵐ[μ] 0

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : Tendsto u atTop (𝓝 0)
u_union : {x | f x ≠ 0} = ⋃ n, {x | u n ≤ f x}
res : μ {x | f x ≠ 0} = 0
⊢ f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this✝ : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ (fs n).range ∧ y ≠ 0
this : (y : β) → Decidable (y = 0) := fun y ↦ Classical.propDecidable (y = 0)
⊢ y ≠ 0

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this✝ : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ (fs n).range ∧ y ≠ 0
this : (y : β) → Decidable (y = 0) := fun y ↦ Classical.propDecidable (y = 0)
⊢ y ≠ 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (bif true then μ else ν) ∧ AEStronglyMeasurable f (bif false then μ else ν) ↔
    AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (bif true then μ else ν) ∧ AEStronglyMeasurable f (bif false then μ else ν) ↔
    AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
⊢ 0 < μ (Function.support f ∩ s) ↔ 0 < μ (Function.support f ∩ s)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ⨆ n, ∫⁻ (a : α), aeSeq hf p n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ⨆ n, ∫⁻ (a : α), aeSeq hf p n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ