a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
⊢ (∫ (x : ℝ) in a..b, Real.log x) = b * Real.log b - a * Real.log a - b + a
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, Real.log x) = b * Real.log b - a * Real.log a - b + a
have h' := fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
heq : ∀ (x : ℝ), x ∈ [[a, b]] → x * x⁻¹ = 1
⊢ (∫ (x : ℝ) in a..b, Real.log x) = b * Real.log b - a * Real.log a - b + a
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
⊢ (∫ (x : ℝ) in a..b, Real.log x) = b * Real.log b - a * Real.log a - b + a
have heq := fun x hx => mul_inv_cancel (h' x hx)
no goals
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
heq : ∀ (x : ℝ), x ∈ [[a, b]] → x * x⁻¹ = 1
⊢ (∫ (x : ℝ) in a..b, Real.log x) = b * Real.log b - a * Real.log a - b + a
convert integral_mul_deriv_eq_deriv_mul (fun x hx => hasDerivAt_log (h' x hx))
  (fun x _ => hasDerivAt_id x) (continuousOn_inv₀.mono <|
    subset_compl_singleton_iff.mpr h).intervalIntegrable
      continuousOn_const.intervalIntegrable using 1 <;>
simp [integral_congr heq, mul_comm, ← sub_add]