α : Type ?u.5138263
β : Type u_1
E : Type ?u.5138269
F : Type ?u.5138272
inst✝¹ : MeasurableSpace α
ι : Type ?u.5138278
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
g : SimpleFunc β ℝ
hf : Integrable f
⊢ Integrable (↑(SimpleFunc.toLargerSpace hm g) * f)
α : Type ?u.5138263
β : Type u_1
E : Type ?u.5138269
F : Type ?u.5138272
inst✝¹ : MeasurableSpace α
ι : Type ?u.5138278
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
g : SimpleFunc β ℝ
hf : Integrable f
⊢ Integrable (↑g * f)
rw [← SimpleFunc.coe_toLargerSpace_eq hm g]
no goals
α : Type ?u.5138263
β : Type u_1
E : Type ?u.5138269
F : Type ?u.5138272
inst✝¹ : MeasurableSpace α
ι : Type ?u.5138278
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
g : SimpleFunc β ℝ
hf : Integrable f
⊢ Integrable (↑(SimpleFunc.toLargerSpace hm g) * f)
exact hf.simpleFunc_mul (g.toLargerSpace hm)