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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f g : α →ₛ F
h : 0 ≤ᵐ[μ] ⇑g - ⇑f
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
⊢ 0 ≤ integral μ (g - f)

Tactic:
]

Goal state after:
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f g : α →ₛ F
h : 0 ≤ᵐ[μ] ⇑g - ⇑f
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
⊢ 0 ≤ integral μ (g - f)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ eLpNorm (↑↑↑((x n).toLp ⋯) - ↑↑↑g) p μ) atTop (𝓝 0)

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ eLpNorm (↑↑↑((x n).toLp ⋯) - ↑↑↑g) p μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
⊢ μ (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0

Tactic:
]

Goal state after:
α : 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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
⊢ μ (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h✝ : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
z : α
h : f z = x ∧ g z = y
⊢ ¬x = y

Tactic:
]

Goal state after:
α : 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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h✝ : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
z : α
h : f z = x ∧ g z = y
⊢ ¬x = y
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
n : ℕ
⊢ ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : 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
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
x✝ : x ∈ f.range
hx0 : ¬x = 0
⊢ (T' (⇑f ⁻¹' {x})) x = (T' (⇑f ⁻¹' {x})) x

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : ¬0 ≤ f x
⊢ ν (⇑f ⁻¹' {f x}) ≤ ν {a | ¬0 a ≤ f a}

Tactic:
]

Goal state after:
case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : ¬0 ≤ f x
⊢ ν (⇑f ⁻¹' {f x}) ≤ ν {a | ¬0 a ≤ f a}
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] E)
⊢ ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖ =
    ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) • ‖x‖

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] E)
⊢ ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖ =
    ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) • ‖x‖
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
h_pos : 0 ≤ᵐ[μ] ⇑(toSimpleFunc f)
⊢ (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f) a) ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f) a) ∂μ).toReal

Tactic:
]

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

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' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T'' (⇑f ⁻¹' {x})) x = ∑ x ∈ f.range with x ≠ 0, ((T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x)

Tactic:
]

Goal state after:
α : 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' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T'' (⇑f ⁻¹' {x})) x = ∑ x ∈ f.range with x ≠ 0, ((T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : ↥(α →₁ₛ[μ] E)
⊢ ‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤
    MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : ↥(α →₁ₛ[μ] E)
⊢ ‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤
    MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁵ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
f : ↥(α →₁ₛ[μ] E)
⊢ ‖f‖ ≤ ‖f‖

Tactic:
]

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

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' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ (T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})) x = (T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x

Tactic:
]

Goal state after:
α : 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' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ (T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})) x = (T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ (T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x = (T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x

Tactic:
]

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

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
a✝¹ : α
a✝ : (toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = max (↑↑↑f a✝¹) 0
h₃ : (toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ max (↑↑↑f a✝¹) 0 = max (↑↑↑f a✝¹) 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
a : α
h : (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
⊢ max ((toSimpleFunc f) a) 0 = max ((toSimpleFunc f) a) 0

Tactic:
]

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

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' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
hx : x ∈ f.range ∧ x ≠ 0
⊢ x ≠ 0

Tactic:
]

Goal state after:
α : 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' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
hx : x ∈ f.range ∧ x ≠ 0
⊢ x ≠ 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
⊢ ⇑(toSimpleFunc (posPart (-f))) =ᵐ[μ] ⇑(-toSimpleFunc f).posPart

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
⊢ ⇑(toSimpleFunc (posPart (-f))) =ᵐ[μ] ⇑(-toSimpleFunc f).posPart
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (-f)).posPart a = (-toSimpleFunc f).posPart a

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (-f)).posPart a = (-toSimpleFunc f).posPart a
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ max ((-⇑(toSimpleFunc f)) a) 0 = max ((-toSimpleFunc f) a) 0

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ max ((-⇑(toSimpleFunc f)) a) 0 = max ((-toSimpleFunc f) a) 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x = ∑ x ∈ f.range with x ≠ 0, c • (T (⇑f ⁻¹' {x})) x

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x = ∑ x ∈ f.range with x ≠ 0, c • (T (⇑f ⁻¹' {x})) x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = ‖(toSimpleFunc f).posPart a✝‖

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = ‖(toSimpleFunc f).posPart a✝‖
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ c • (T (⇑f ⁻¹' {x})) x = c • (T (⇑f ⁻¹' {x})) x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
⊢ (toSimpleFunc f).negPart a✝ = ‖(toSimpleFunc f).negPart a✝‖

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
⊢ (toSimpleFunc f).negPart a✝ = ‖(toSimpleFunc f).negPart a✝‖
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
hx : x ∈ f.range ∧ x ≠ 0
⊢ x ≠ 0

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
hx : x ∈ f.range ∧ x ≠ 0
⊢ x ≠ 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) (x.1 + x.2) =
    ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) (x.1 + x.2)

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ 0.1 + 0.2 = 0

Tactic:
]

Goal state after:
α : 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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ 0.1 + 0.2 = 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2 =
    ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))

pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))) μ

pp: case hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))) μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))) μ

case hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))) μ
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (-x) = ∑ x ∈ f.range, -(T (⇑f ⁻¹' {x})) x

Tactic:
]

Goal state after:
α : 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
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (-x) = ∑ x ∈ f.range, -(T (⇑f ⁻¹' {x})) x