no goals
E : Type ?u.35816
F : Type ?u.35819
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b : ℝ
⊢ IntervalIntegrable (fun x => x⁻¹) volume a b ↔ a = b ∨ ¬0 ∈ [[a, b]]
simp only [← intervalIntegrable_sub_inv_iff, sub_zero]