Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_2
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u u' : X → E
a✝ : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun x ↦ ↑(f x))
u'_int : Integrable u' (μ.withDensity fun x ↦ ↑(f x))
h : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
h' : (∫ (x : X), u' x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u' x ∂μ
⊢ ∫ (x : X), f x • u x ∂μ + ∫ (x : X), f x • u' x ∂μ = ∫ (a : X), f a • u a ∂μ + ∫ (a : X), f a • u' a ∂μ

pp: case pos.refine_2.hf
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u u' : X → E
a✝ : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun x ↦ ↑(f x))
u'_int : Integrable u' (μ.withDensity fun x ↦ ↑(f x))
h : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
h' : (∫ (x : X), u' x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u' x ∂μ
⊢ Integrable (fun x ↦ f x • u x) μ

pp: case pos.refine_2.hg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u u' : X → E
a✝ : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun x ↦ ↑(f x))
u'_int : Integrable u' (μ.withDensity fun x ↦ ↑(f x))
h : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
h' : (∫ (x : X), u' x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u' x ∂μ
⊢ Integrable (fun x ↦ f x • u' x) μ

Tactic:
]

Goal state after:
case pos.refine_2.hf
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u u' : X → E
a✝ : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun x ↦ ↑(f x))
u'_int : Integrable u' (μ.withDensity fun x ↦ ↑(f x))
h : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
h' : (∫ (x : X), u' x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u' x ∂μ
⊢ Integrable (fun x ↦ f x • u x) μ

case pos.refine_2.hg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u u' : X → E
a✝ : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun x ↦ ↑(f x))
u'_int : Integrable u' (μ.withDensity fun x ↦ ↑(f x))
h : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
h' : (∫ (x : X), u' x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u' x ∂μ
⊢ Integrable (fun x ↦ f x • u' x) μ