Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hu : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x = f x • ↑↑v x
huv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯) x = f x • ↑↑(u + v) x
h' :
  ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x =
    (↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) + ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯)) x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x ≠ 0
⊢ f x • (↑↑u x + ↑↑v x) = f x • ↑↑u x + f x • ↑↑v x

pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hu : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x = f x • ↑↑v x
huv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯) x = f x • ↑↑(u + v) x
h' :
  ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x =
    (↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) + ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯)) x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x ≠ 0
⊢ ↑(f x) ≠ 0

Tactic:
smul_add

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hu : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x = f x • ↑↑v x
huv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯) x = f x • ↑↑(u + v) x
h' :
  ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x =
    (↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) + ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯)) x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x ≠ 0
⊢ f x • ↑↑u x + f x • ↑↑v x = f x • ↑↑u x + f x • ↑↑v x

α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hu : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x = f x • ↑↑v x
huv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯) x = f x • ↑↑(u + v) x
h' :
  ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x =
    (↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) + ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯)) x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x ≠ 0
⊢ ↑(f x) ≠ 0