no goals
α : Type u_1
E : Type ?u.1088155
F : Type ?u.1088158
𝕜 : Type ?u.1088161
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1090852
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
b : ℝ≥0
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) ≤ ↑b ↔ (∫ (a : α), ↑(f a) ∂μ) ≤ ↑b
rw [lintegral_coe_eq_integral f hfi, ENNReal.ofReal, ENNReal.coe_le_coe,
  Real.toNNReal_le_iff_le_coe]