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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝² : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h✝¹ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h✝ : (toSimpleFunc g) a✝ = ↑↑↑g a✝
h : ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝
⊢ ↑↑↑f a✝ - ↑↑↑g a✝ = ↑↑↑f a✝ - ↑↑↑g a✝

Tactic:
]

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

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • (toSimpleFunc f) a✝

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • (toSimpleFunc f) a✝
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0

Tactic:
]

Goal state after:
α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝
⊢ k • ↑↑↑f a✝ = k • ↑↑↑f a✝

Tactic:
]

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

Goal state before:
pp: case inr
α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ (T (⇑f ⁻¹' {x})) x = 0

Tactic:
]

Goal state after:
case inr
α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ (T (⇑f ⁻¹' {x})) x = 0
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f : ↥(simpleFunc E p μ)
this : ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (f.toLp hf)
⊢ P ((toSimpleFunc f).toLp ⋯)

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f : ↥(simpleFunc E p μ)
this : ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (f.toLp hf)
⊢ P ((toSimpleFunc f).toLp ⋯)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case inr
α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ (T ∅) x = 0

pp: case inr
α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ Disjoint {x} (Set.range ⇑f)

Tactic:
]

Goal state after:
case inr
α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ (T ∅) x = 0

case inr
α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ Disjoint {x} (Set.range ⇑f)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case pos
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
⊢ 0 = 0

pp: α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
x : G
hx : x ∈ {x ∈ f.range | g x = 0}
⊢ (T (⇑f ⁻¹' {x})) (g x) = 0

Tactic:
]

Goal state after:
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
x : G
hx : x ∈ {x ∈ f.range | g x = 0}
⊢ (T (⇑f ⁻¹' {x})) (g x) = 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
x : G
hx : x ∈ f.range ∧ g x = 0
⊢ (T (⇑f ⁻¹' {x})) (g x) = 0

Tactic:
]

Goal state after:
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
x : G
hx : x ∈ f.range ∧ g x = 0
⊢ (T (⇑f ⁻¹' {x})) (g x) = 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
x : G
hx : x ∈ f.range ∧ g x = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
⊢ (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
⊢ (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) = ∑ j ∈ f.range with g j = g (f a), (T (⇑f ⁻¹' {j})) (g j)

Tactic:
]

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
⊢ (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) = ∑ j ∈ f.range with g j = g (f a), (T (⇑f ⁻¹' {j})) (g j)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
⊢ IsDenseEmbedding Subtype.val

Tactic:
borelize E

Goal state after:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ IsDenseEmbedding Subtype.val
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
⊢ (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a)) =
    (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a))

Tactic:
]

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f : ↥(Lp E p μ)
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range Subtype.val) ∧ Tendsto x atTop (𝓝 f)

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f : ↥(Lp E p μ)
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range Subtype.val) ∧ Tendsto x atTop (𝓝 f)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑↑f) p μ
this : SeparableSpace ↑(Set.range ↑↑f ∪ {0})
⊢ f = f

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) =
    (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a))
⊢ (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a)) =
    ∑ j ∈ f.range with g j = g (f a), (T (⇑f ⁻¹' {j})) (g j)

Tactic:
]

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) =
    (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a))
⊢ (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a)) =
    ∑ j ∈ f.range with g j = g (f a), (T (⇑f ⁻¹' {j})) (g j)
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
f g : ↥(simpleFunc G p μ)
⊢ ↑↑↑f ≤ᵐ[μ] ↑↑↑g ↔ ↑↑↑f ≤ᵐ[μ] ↑↑↑g

Tactic:
]

Goal state after:
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 α
x : F
⊢ μ.real ∅ • x = 0 x

Tactic:
]

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ μ.real ∅ • x = 0 x
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
f : ↥(simpleFunc G p μ)
⊢ 0 ≤ ↑f ↔ 0 ≤ ↑f

Tactic:
]

Goal state after:
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 α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
x : F
⊢ μ.real s • x + ν.real s • x = μ.real s • x + ν.real s • x

Tactic:
]

Goal state after:
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
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᵐ[μ] ⇑g
x : α
hx : 0 ≤ g x
⊢ g x = (SimpleFunc.map ({x | 0 ≤ x}.piecewise id 0) g) x

Tactic:
simpa using! Set.indicator_of_mem hx id |>.symm

Goal state after:
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 α
s : Set α
h_zero : μ s = 0
x : F
⊢ ENNReal.toReal 0 • x = 0 x

Tactic:
]

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : μ s = 0
x : F
⊢ ENNReal.toReal 0 • x = 0 x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ f.posPart a✝ = f.posPart a✝

pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ 0 ≤ f.posPart a✝

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ 0 ≤ f.posPart a✝
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (-f).posPart = (-f).posPart

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (-f).posPart = (-f).posPart
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
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)

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
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ (⇑(map (fun b ↦ max b 0) f) - ⇑(map (fun b ↦ max b 0) (-f))) a = f a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ (⇑(map (fun b ↦ max b 0) f) - ⇑(map (fun b ↦ max b 0) (-f))) a = f a
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✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
⊢ ∑ x ∈ s, μ.real (⇑f ⁻¹' {x}) • x = ∑ x ∈ s, μ.real (⇑f ⁻¹' {x}) • x

pp: α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
⊢ ∀ x ∈ s, x ∉ {x ∈ f.range | x ≠ 0} → μ.real (⇑f ⁻¹' {x}) • x = 0

Tactic:
]

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
⊢ ∀ x ∈ s, x ∉ {x ∈ f.range | x ≠ 0} → μ.real (⇑f ⁻¹' {x}) • x = 0
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✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0

Tactic:
]

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case inr
α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0

Tactic:
]

Goal state after:
case inr
α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0