mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_4
inst✝⁵ : NormedDivisionRing 𝕜
G : Type u_5
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝² : Module 𝕜 G
inst✝¹ : NormSMulClass 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
⊢ ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
𝕜 : Type u_4
inst✝⁵ : NormedDivisionRing 𝕜
G : Type u_5
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝² : Module 𝕜 G
inst✝¹ : NormSMulClass 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
⊢ (setToFun μ (weightedSMul μ) ⋯ fun a ↦ c • f a) = c • setToFun μ (weightedSMul μ) ⋯ f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᵐ[μ] g
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᵐ[μ] g
⊢ setToFun μ (weightedSMul μ) ⋯ f = setToFun μ (weightedSMul μ) ⋯ g
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
⊢ ∫ (a : α), ↑(AEEqFun.mk f ⋯) a ∂μ = ∫ (a : α), f a ∂μ

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
⊢ setToFun μ (weightedSMul μ) ⋯ ↑(AEEqFun.mk f ⋯) = setToFun μ (weightedSMul μ) ⋯ f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ ∫ (a : α), ↑↑f a ∂μ

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ setToFun μ (weightedSMul μ) ⋯ ↑↑f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖setToFun μ (weightedSMul μ) ⋯ f‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖∫ (a : α), f a ∂μ‖ₑ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖setToFun μ (weightedSMul μ) ⋯ f‖ₑ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case h
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F' →L[ℝ] F
f : α →ₛ F'
b : F'
a✝ : b ∈ f.range
⊢ ‖(T (⇑f ⁻¹' {b})) b‖ ≤ ‖T (⇑f ⁻¹' {b})‖ * ‖b‖

Tactic:
apply ContinuousLinearMap.le_opNorm

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i ↦ ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i ↦ setToFun μ (weightedSMul μ) ⋯ (F i)) l (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case refine_2
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
⊢ Tendsto (fun i ↦ ∫⁻ (x : α) in s, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
simp_rw [← eLpNorm_one_eq_lintegral_enorm] at hF ⊢

Goal state after:
case refine_2
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
s : Set α
hF : Tendsto (fun i ↦ eLpNorm (fun x ↦ F i x - f x) 1 μ) l (𝓝 0)
⊢ Tendsto (fun i ↦ eLpNorm (fun x ↦ F i x - f x) 1 (μ.restrict s)) l (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x ↦ F x a) s x₀
⊢ ContinuousWithinAt (fun x ↦ ∫ (a : α), F x a ∂μ) s x₀

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x ↦ F x a) s x₀
⊢ ContinuousWithinAt (fun x ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) s x₀
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun x ↦ F x a) x₀
⊢ ContinuousAt (fun x ↦ ∫ (a : α), F x a ∂μ) x₀

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun x ↦ F x a) x₀
⊢ ContinuousAt (fun x ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) x₀
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
s : Set X
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x ↦ F x a) s
⊢ ContinuousOn (fun x ↦ ∫ (a : α), F x a ∂μ) s

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
s : Set X
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x ↦ F x a) s
⊢ ContinuousOn (fun x ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) s
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) μ
h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ F x a
⊢ Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ ∫ (a : α), F x a ∂μ

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) μ
h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ F x a
⊢ Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ setToFun μ (weightedSMul μ) ⋯ (F x)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
⊢ (u - v + (t - w)) =o[l] (v + w)

Tactic:
change (fun x ↦ (u - v) x + (t - w) x) =o[l] (fun x ↦ v x + w x)

Goal state after:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
⊢ (fun x ↦ (u - v) x + (t - w) x) =o[l] fun x ↦ v x + w x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case hfi
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ Integrable (fun a ↦ f i a - f 0 a) μ

Tactic:
exact (hf_int i).sub (hf_int 0)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  by_cases hf : Integrable f μ
  · simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left T T' hT hT' h]
  · simp_rw [setToFun_undef _ hf]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : ¬Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ (∫ (x : X), f x ∂Measure.sum fun i ↦ c i • Measure.dirac (x i)) = ∑' (i : ι), (c i).toReal • f (x i)

Tactic:
rw [integral_undef hf, tsum_eq_zero_of_not_summable]

Goal state after:
case neg
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : ¬Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ ¬Summable fun i ↦ (c i).toReal • f (x i)
Module: Mathlib.Topology.Algebra.Indicator

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
· exact ContinuousAt.congr continuousAt_const <| Filter.eventuallyEq_iff_exists_mem.mpr
      ⟨sᶜ, mem_interior_iff_mem_nhds.mp h, Set.eqOn_mulIndicator'.symm⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s✝ : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ Integrable (∑ i ∈ s, f i) μ

Tactic:
· convert! integrable_finsetSum s fun i hi => hf i (Finset.mem_insert_of_mem hi) with x
      simp

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : IsFiniteMeasure μ
⊢ ∫ (x : α), c ∂μ = μ.real univ • c

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : IsFiniteMeasure μ
⊢ (setToFun μ (weightedSMul μ) ⋯ fun a ↦ c) = μ.real univ • c
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
⊢ ∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
⊢ setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
⊢ ∫ (x : α), f x ∂0 = 0

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
⊢ setToFun 0 (weightedSMul 0) ⋯ f = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hc : c ≠ ∞
hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal
hdfma_smul : DominatedFinMeasAdditive (c • μ) (weightedSMul (c • μ)) 1
⊢ setToFun μ (weightedSMul (c • μ)) hdfma f = setToFun μ (fun s ↦ c.toReal • weightedSMul μ s) ⋯ f

Tactic:
exact setToFun_congr_left' _ _ (fun s _ _ => weightedSMul_smul_measure μ c) f

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

Goal state before:
pp: case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : Integrable f (Measure.map φ μ)
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

Tactic:
simp only [integral_eq_setToFun]

Goal state after:
case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : Integrable f (Measure.map φ μ)
⊢ setToFun (Measure.map φ μ) (weightedSMul (Measure.map φ μ)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ fun a ↦ f (φ a)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Continuous[Pi.topologicalSpace, topologicalSpace]
    (LinearMap.toContinuousLinearMap.symm ≪≫ₗ LinearEquiv.piRing 𝕜 E ι 𝕜).invFun

Tactic:
by
      simp_rw [LinearEquiv.invFun_eq_symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
      refine AddMonoidHomClass.continuous_of_bound
        (LinearMap.toContinuousLinearMap.toLinearMap.comp
            (LinearEquiv.piRing 𝕜 E ι 𝕜).symm.toLinearMap)
        (Fintype.card ι : ℝ) fun g ↦ ?_
      rw [← nsmul_eq_mul]
      refine opNorm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t ↦ ?_
      simp_rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply,
        LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply]
      apply le_trans (norm_sum_le _ _)
      rw [smul_mul_assoc]
      refine Finset.sum_le_card_nsmul _ _ _ fun i _ ↦ ?_
      rw [norm_smul, mul_comm]
      gcongr <;> apply norm_le_pi_norm

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁸ : NormedAddCommGroup G''
inst✝⁷ : PartialOrder G''
inst✝⁶ : IsOrderedAddMonoid G''
inst✝⁵ : NormedSpace ℝ G''
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : PartialOrder G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : ClosedIciTopology G''
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ 0 ≤ g a - f a

Tactic:
sub_nonneg

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁸ : NormedAddCommGroup G''
inst✝⁷ : PartialOrder G''
inst✝⁶ : IsOrderedAddMonoid G''
inst✝⁵ : NormedSpace ℝ G''
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : PartialOrder G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : ClosedIciTopology G''
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ f a ≤ g a
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case hp_ne_zero
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ ENNReal.ofReal q ≠ 0

Tactic:
rw [Ne, ENNReal.ofReal_eq_zero, not_le]
        exact hpq.symm.pos

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ ENNReal.ofReal |(thickenedIndicatorAux δ E x).toReal - (thickenedIndicatorAux δ E y).toReal| ≤
    ↑δ.toNNReal⁻¹ * edist x y

Tactic:
← ENNReal.toReal_sub_of_le (thickenedIndicatorAux_mono_infEDist _ h) (by finiteness)

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ ENNReal.ofReal |(thickenedIndicatorAux δ E x - thickenedIndicatorAux δ E y).toReal| ≤ ↑δ.toNNReal⁻¹ * edist x y
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ - ∫ (a : α), ↑(-f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

Tactic:
sub_nonneg

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ y, Tendsto f (𝓝[<] c) (𝓝 y)
⊢ leftLim f c ∈ id s

Tactic:
apply s_closed.mem_of_tendsto (tendsto_leftLim_of_tendsto h''c)

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ y, Tendsto f (𝓝[<] c) (𝓝 y)
⊢ ∀ᶠ (x : α) in 𝓝[<] c, f x ∈ s
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
⊢ ∫ (x : X) in univ, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
← setIntegral_congr_set

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
⊢ ∫ (x : X) in ?m.43, f x ∂μ = ∫ (x : X) in s, f x ∂μ

X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
⊢ ?m.43 =ᵐ[μ] univ

X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
⊢ Set X