no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
h : ∀ (x : ℝ), x ∈ [[a, b]] → f x ≠ 0
hf : ContinuousOn f [[a, b]]
⊢ IntervalIntegrable (fun x => (f x)⁻¹) μ a b
simpa only [one_div] using intervalIntegrable_one_div h hf