import Mathlib.Analysis.SpecialFunctions.Integrals

theorem intervalIntegral.intervalIntegrable_log'
  {a : ℝ}
  {b : ℝ}
  {μ : MeasureTheory.Measure ℝ}
  [MeasureTheory.IsLocallyFiniteMeasure μ]
  (ha : 0 < a) :
  IntervalIntegrable Real.log μ 0 a
  := by

  sorry

theorem integral_log₀
  {b : ℝ}
  (hb : 0 < b) :
  ∫ (x : ℝ) in (0)..b, Real.log x = b * (Real.log b - 1) := by
  apply?
  exact integral_log h


open Real Nat Set Finset

open scoped Real Interval

--variable {a b : ℝ} (n : ℕ)

namespace intervalIntegral

--open MeasureTheory

--variable {f : ℝ → ℝ} {μ ν : Measure ℝ} [IsLocallyFiniteMeasure μ] (c d : ℝ)

#check integral_mul_deriv_eq_deriv_mul

theorem integral_log₁
  (h : (0 : ℝ) ∉ [[a, b]]) :
  ∫ x in a..b, log x = b * log b - a * log a - b + a := by

  have h' : ∀ x ∈ [[a, b]], x ≠ 0 :=
    fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
  have heq :  ∀ x ∈ [[a, b]], x * x⁻¹ = 1 :=
    fun x hx => mul_inv_cancel (h' x hx)

  let A := fun x hx => hasDerivAt_log (h' x hx)

  convert integral_mul_deriv_eq_deriv_mul A (fun x _ => hasDerivAt_id x)

  convert integral_mul_deriv_eq_deriv_mul A
    (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]