case inl
α : Type u_2
β : Type u_1
γ : Type ?u.851862
δ : Type ?u.851865
m : MeasurableSpace α
ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
⊢ Integrable f

case inr
α : Type u_2
β : Type u_1
γ : Type ?u.851862
δ : Type ?u.851865
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
hne : μ ≠ 0
⊢ Integrable f
α : Type u_2
β : Type u_1
γ : Type ?u.851862
δ : Type ?u.851865
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
⊢ Integrable f
rcases eq_or_ne μ 0 with (rfl | hne)
no goals
case inl
α : Type u_2
β : Type u_1
γ : Type ?u.851862
δ : Type ?u.851865
m : MeasurableSpace α
ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
⊢ Integrable f
rwa [smul_zero]
case inr
α : Type u_2
β : Type u_1
γ : Type ?u.851862
δ : Type ?u.851865
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
hne : μ ≠ 0
⊢ (↑↑μ univ)⁻¹ ≠ ⊤
case inr
α : Type u_2
β : Type u_1
γ : Type ?u.851862
δ : Type ?u.851865
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
hne : μ ≠ 0
⊢ Integrable f
apply h.smul_measure
no goals
case inr
α : Type u_2
β : Type u_1
γ : Type ?u.851862
δ : Type ?u.851865
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
hne : μ ≠ 0
⊢ (↑↑μ univ)⁻¹ ≠ ⊤
simpa