awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
this :
  Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
h₁ : ∀ (h' : -1 < (↑r : ℂ).re), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b
h₂ :
  ∀ (h' : (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]),
    IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b

Tactic:
rcases h' with h' | h'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this :
  Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
h' : -1 < (↑r : ℂ).re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b

Tactic:
intervalIntegrable_cpow' h'

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this :
  Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
h' : -1 < (↑r : ℂ).re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b

Tactic:
exact intervalIntegrable_cpow' h'

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this :
  Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
h' : (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b

Tactic:
intervalIntegrable_cpow (Or.inr h'.2)

Premises used: intervalIntegral.intervalIntegrable_cpow, And.right, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this :
  Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
h' : (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b

Tactic:
exact intervalIntegrable_cpow (Or.inr h'.2)

Premises used: intervalIntegral.intervalIntegrable_cpow, And.right, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
this :
  Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
push_cast : (↑r : ℂ) + 1 = (↑r : ℂ) + 1
⊢ (↑r : ℂ) + 1 = (↑(r + 1) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
this :
  Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
⊢ (↑r : ℂ) + 1 = (↑r : ℂ) + 1

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
this :
  Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
h₁ :
  (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = (((↑b : ℂ) ^ (↑(r + 1) : ℂ) - (↑a : ℂ) ^ (↑(r + 1) : ℂ)) / (↑(r + 1) : ℂ)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re

Tactic:
rw [(by push_cast; rfl : (r : ℂ) + 1 = ((r + 1 : ℝ) : ℂ))]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
this :
  Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
h₁ :
  (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) =
    ((↑(r + 1) : ℂ)⁻¹ * ((↑b : ℂ) ^ (↑(r + 1) : ℂ) - (↑a : ℂ) ^ (↑(r + 1) : ℂ))).re
h₂ :
  (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) =
    ((↑(r + 1)⁻¹ : ℂ) * ((↑b : ℂ) ^ (↑(r + 1) : ℂ) - (↑a : ℂ) ^ (↑(r + 1) : ℂ))).re
h₃ : (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * ((↑b : ℂ) ^ (↑(r + 1) : ℂ) - (↑a : ℂ) ^ (↑(r + 1) : ℂ)).re
h₄ :
  (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) =
    (r + 1)⁻¹ * (((↑b : ℂ) ^ (↑(r + 1) : ℂ)).re - ((↑a : ℂ) ^ (↑(r + 1) : ℂ)).re)
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = (((↑b : ℂ) ^ (↑(r + 1) : ℂ) - (↑a : ℂ) ^ (↑(r + 1) : ℂ)) / (↑(r + 1) : ℂ)).re

Tactic:
simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.re_ofReal_mul, Complex.sub_re, rpow_def]

Premises used: Complex.sub_re, div_eq_inv_mul, Complex.ofReal_inv, Real.rpow_def, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ LT.lt (α := ℝ) (-1) (↑n : ℝ) ∨ Ne (α := ℝ) (↑n : ℝ) (-1) ∧ 0 ∉ [[a, b]]

Tactic:
replace h : -1 < (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] := mod_cast h
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℤ
h : LT.lt (α := ℝ) (-1) (↑n : ℝ) ∨ Ne (α := ℝ) (↑n : ℝ) (-1) ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
mod_cast integral_rpow h

Premises used: Int.cast, congrArg, HSub.hSub, intervalIntegral, cast, HDiv.hDiv, Nat.cast, funext, integral_rpow, HPow.hPow, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, congr, Int.cast_add._simp_1, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Real.rpow_intCast, Int.cast_one, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℤ
h : LT.lt (α := ℝ) (-1) (↑n : ℝ) ∨ Ne (α := ℝ) (↑n : ℝ) (-1) ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
exact mod_cast integral_rpow h

Premises used: integral_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simpa only [← Int.natCast_succ, zpow_natCast] using integral_zpow (Or.inl n.cast_nonneg)

Premises used: zpow_natCast, Nat.cast_nonneg, Int.natCast_succ, integral_zpow, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
inl :
  ∀ (hab : a ≤ b),
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
        (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) fun (x : ℝ) ↦ |x - a| ^ n) =
      |b - a| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
inr :
  ∀ (hab : b < a),
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
        (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) fun (x : ℝ) ↦ |x - a| ^ n) =
      |b - a| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) fun (x : ℝ) ↦ |x - a| ^ n) =
    |b - a| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
rcases le_or_gt a b with hab | hab

Premises used: le_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
rw :
  Eq (α := ℝ)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Set.Ioc a b)) fun (x : ℝ) ↦ |x - a| ^ n)
    (∫ (x : ℝ) in a..b, |x - a| ^ n)
rw₁ rw₂ : Eq (α := ℝ) (∫ (x : ℝ) in a..b, |x - a| ^ n) (∫ (x : ℝ) in a..b, |x - a| ^ n)
⊢ Eq (α := ℝ)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) fun (x : ℝ) ↦ |x - a| ^ n)
    (∫ (x : ℝ) in a..b, |x - a| ^ n)

Tactic:
rw [uIoc_of_le hab, ← integral_of_le hab]

Premises used: intervalIntegral.integral_of_le, Set.uIoc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
simp : Eq (α := ℝ) (∫ (x : ℝ) in 0..b - a, |x| ^ n) (∫ (x : ℝ) in 0..b - a, x ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, |x - a| ^ n) (∫ (x : ℝ) in 0..b - a, x ^ n)

Tactic:
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]

Premises used: sub_self, abs, intervalIntegral.integral_comp_sub_right, HPow.hPow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..b - a, |x| ^ n) (∫ (x : ℝ) in 0..b - a, x ^ n)

Tactic:
integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| ?_) rfl

Premises used: intervalIntegral.integral_congr, Pow.pow, abs_of_nonneg, rfl, congr_arg₂
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
refine : ∀ (x : ℝ) (hx : x ∈ [[0, b - a]]), 0 ≤ x
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..b - a, |x| ^ n) (∫ (x : ℝ) in 0..b - a, x ^ n)

Tactic:
refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| ?_) rfl

Premises used: intervalIntegral.integral_congr, Pow.pow, abs_of_nonneg, rfl, congr_arg₂
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ [[0, b - a]]
⊢ x ∈ Set.Icc 0 (b - a)

Tactic:
rw [uIcc_of_le (sub_nonneg.2 hab)] at hx

Premises used: Iff.mpr, Set.uIcc_of_le, sub_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ Set.Icc 0 (b - a)
⊢ 0 ≤ x

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ Set.Icc 0 (b - a)
⊢ 0 ≤ x

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in 0..b - a, x ^ n = |b - a| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp [abs_of_nonneg (sub_nonneg.2 hab)]

Premises used: Iff.mpr, abs_of_nonneg, sub_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
x :
  Eq (α := ℝ)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) fun (x : ℝ) ↦ |x - a| ^ n)
    (∫ (x : ℝ) in a..b, |x - a| ^ n)
x₁ : Eq (α := ℝ) (∫ (x : ℝ) in a..b, |x - a| ^ n) (∫ (x : ℝ) in 0..b - a, x ^ n)
x₂ : ∫ (x : ℝ) in 0..b - a, x ^ n = |b - a| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) fun (x : ℝ) ↦ |x - a| ^ n) =
    |b - a| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
calc
      ∫ x in Ι a b, |x - a| ^ n = ∫ x in a..b, |x - a| ^ n := by
        rw [uIoc_of_le hab, ← integral_of_le hab]
      _ = ∫ x in 0..(b - a), x ^ n := by
        simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
        refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| ?_) rfl
        rw [uIcc_of_le (sub_nonneg.2 hab)] at hx
        exact hx.1
      _ = |b - a| ^ (n + 1) / (n + 1) := by simp [abs_of_nonneg (sub_nonneg.2 hab)]

Premises used: Set.uIoc, HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : b < a
rw :
  Eq (α := ℝ)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Set.Ioc b a)) fun (x : ℝ) ↦ |x - a| ^ n)
    (∫ (x : ℝ) in b..a, |x - a| ^ n)
rw₁ rw₂ : Eq (α := ℝ) (∫ (x : ℝ) in b..a, |x - a| ^ n) (∫ (x : ℝ) in b..a, |x - a| ^ n)
⊢ Eq (α := ℝ)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) fun (x : ℝ) ↦ |x - a| ^ n)
    (∫ (x : ℝ) in b..a, |x - a| ^ n)

Tactic:
rw [uIoc_of_ge hab.le, ← integral_of_le hab.le]

Premises used: LT.lt.le, intervalIntegral.integral_of_le, Set.uIoc_of_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : b < a
simp : Eq (α := ℝ) (∫ (x : ℝ) in b - a..0, |x| ^ n) (∫ (x : ℝ) in b - a..0, (-x) ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in b..a, |x - a| ^ n) (∫ (x : ℝ) in b - a..0, (-x) ^ n)

Tactic:
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]

Premises used: sub_self, abs, intervalIntegral.integral_comp_sub_right, HPow.hPow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : b < a
⊢ Eq (α := ℝ) (∫ (x : ℝ) in b - a..0, |x| ^ n) (∫ (x : ℝ) in b - a..0, (-x) ^ n)

Tactic:
integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| ?_) rfl

Premises used: intervalIntegral.integral_congr, Pow.pow, abs_of_nonpos, rfl, congr_arg₂
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : b < a
refine : ∀ (x : ℝ) (hx : x ∈ [[b - a, 0]]), x ≤ 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in b - a..0, |x| ^ n) (∫ (x : ℝ) in b - a..0, (-x) ^ n)

Tactic:
refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| ?_) rfl

Premises used: intervalIntegral.integral_congr, Pow.pow, abs_of_nonpos, rfl, congr_arg₂
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ [[b - a, 0]]
⊢ x ∈ Set.Icc (b - a) 0

Tactic:
rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx

Premises used: Iff.mpr, Set.uIcc_of_le, LT.lt.le, sub_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ Set.Icc (b - a) 0
⊢ x ≤ 0

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ Set.Icc (b - a) 0
⊢ x ≤ 0

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in b - a..0, (-x) ^ n = |b - a| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]

Premises used: sub_neg, Iff.mpr, abs_of_neg, HPow.hPow, intervalIntegral.integral_comp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
hab : b < a
x :
  Eq (α := ℝ)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) fun (x : ℝ) ↦ |x - a| ^ n)
    (∫ (x : ℝ) in b..a, |x - a| ^ n)
x₁ : Eq (α := ℝ) (∫ (x : ℝ) in b..a, |x - a| ^ n) (∫ (x : ℝ) in b - a..0, (-x) ^ n)
x₂ : ∫ (x : ℝ) in b - a..0, (-x) ^ n = |b - a| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) fun (x : ℝ) ↦ |x - a| ^ n) =
    |b - a| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
calc
      ∫ x in Ι a b, |x - a| ^ n = ∫ x in b..a, |x - a| ^ n := by
        rw [uIoc_of_ge hab.le, ← integral_of_le hab.le]
      _ = ∫ x in b - a..0, (-x) ^ n := by
        simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
        refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| ?_) rfl
        rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx
        exact hx.2
      _ = |b - a| ^ (n + 1) / (n + 1) := by
        simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]

Premises used: Set.uIoc, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) x 1 =
    (b ^ HAdd.hAdd (α := ℕ) 1 1 - a ^ HAdd.hAdd (α := ℕ) 1 1) / HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1

Tactic:
have := @integral_pow a b 1
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) x 1 =
    (b ^ HAdd.hAdd (α := ℕ) 1 1 - a ^ HAdd.hAdd (α := ℕ) 1 1) / HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1
⊢ ∫ (x : ℝ) in a..b, x = (HPow.hPow (β := ℕ) b 2 - HPow.hPow (β := ℕ) a 2) / 2

Tactic:
norm_num at this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this : ∫ (x : ℝ) in a..b, x = (HPow.hPow (β := ℕ) b 2 - HPow.hPow (β := ℕ) a 2) / 2
⊢ ∫ (x : ℝ) in a..b, x = (HPow.hPow (β := ℕ) b 2 - HPow.hPow (β := ℕ) a 2) / 2

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this : ∫ (x : ℝ) in a..b, x = (HPow.hPow (β := ℕ) b 2 - HPow.hPow (β := ℕ) a 2) / 2
⊢ ∫ (x : ℝ) in a..b, x = (HPow.hPow (β := ℕ) b 2 - HPow.hPow (β := ℕ) a 2) / 2

Tactic:
exact this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, 1 = b - a

Tactic:
simp only [mul_one, smul_eq_mul, integral_const]

Premises used: smul_eq_mul, mul_one, intervalIntegral.integral_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..a + 1, b = b

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h : 0 ∉ [[a, b]]
⊢ ∀ (x : ℝ) (hx : x ∈ [[a, b]]), x ≠ 0

Tactic:
have h' := fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h : 0 ∉ [[a, b]]
h' : ∀ (x : ℝ) (hx : x ∈ [[a, b]]), x ≠ 0
rw : log b - log a = log (b / a)
rw₁ rw₂ : log b - log a = log b - log a
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)

Tactic:
rw [integral_deriv_eq_sub' _ deriv_log' (fun x hx => differentiableAt_log (h' x hx))
      (continuousOn_inv₀.mono <| subset_compl_singleton_iff.mpr h),
    log_div (h' b right_mem_uIcc) (h' a left_mem_uIcc)]

Premises used: Iff.mpr, Set.subset_compl_singleton_iff, Real.differentiableAt_log, Real.deriv_log', Set.right_mem_uIcc, Set.left_mem_uIcc, continuousOn_inv₀, Real.log_div, intervalIntegral.integral_deriv_eq_sub', ContinuousOn.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
ha : 0 < a
hb : 0 < b
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)

Tactic:
integral_inv <| notMem_uIcc_of_lt ha hb

Premises used: Set.notMem_uIcc_of_lt, integral_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
ha : a < 0
hb : b < 0
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)

Tactic:
integral_inv <| notMem_uIcc_of_gt ha hb

Premises used: Set.notMem_uIcc_of_gt, integral_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h : 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, 1 / x = log (b / a)

Tactic:
simp only [one_div, integral_inv h]

Premises used: integral_inv, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
ha : 0 < a
hb : 0 < b
⊢ ∫ (x : ℝ) in a..b, 1 / x = log (b / a)

Tactic:
simp only [one_div, integral_inv_of_pos ha hb]

Premises used: integral_inv_of_pos, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
ha : a < 0
hb : b < 0
⊢ ∫ (x : ℝ) in a..b, 1 / x = log (b / a)

Tactic:
simp only [one_div, integral_inv_of_neg ha hb]

Premises used: integral_inv_of_neg, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
hderiv : deriv rexp = rexp
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x
hcont : ContinuousOn rexp [[a, b]]
⊢ ∫ (x : ℝ) in a..b, rexp x = rexp b - rexp a

Tactic:
rw [integral_deriv_eq_sub']

Premises used: intervalIntegral.integral_deriv_eq_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ deriv rexp = rexp

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x

Tactic:
fun _ _ => differentiableAt_exp

Premises used: Real.differentiableAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x

Tactic:
exact fun _ _ => differentiableAt_exp

Premises used: Real.differentiableAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ContinuousOn rexp [[a, b]]

Tactic:
continuousOn_exp

Premises used: Real.continuousOn_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ContinuousOn rexp [[a, b]]

Tactic:
exact continuousOn_exp

Premises used: Real.continuousOn_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
f : fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c
f' : Complex.exp (c * (↑x : ℂ))
x₁ : x
| HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
rw : HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ)) * c / c) x
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x

Tactic:
rw [← mul_div_cancel_right₀ (Complex.exp (c * x)) hc]

Premises used: HMul.hMul, Complex.ofReal, mul_div_cancel_right₀, Complex.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
apply : HasDerivAt (fun (x : ℝ) ↦ c * (↑x : ℂ)) c x
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ)) * c / c) x

Tactic:
apply ((Complex.hasDerivAt_exp _).comp x _).div_const c

Premises used: HasDerivAt.comp, HasDerivAt.div_const, Complex.hasDerivAt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ c * (↑x : ℂ)) c x

Tactic:
simpa only [mul_one] using ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal

Premises used: HasDerivAt.comp_ofReal, Complex.ofReal, hasDerivAt_id, HasDerivAt.const_mul, mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
⊢ ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x

Tactic:
have D : ∀ x : ℝ, HasDerivAt (fun y : ℝ => Complex.exp (c * y) / c) (Complex.exp (c * x)) x := by
    intro x
    conv => congr
    rw [← mul_div_cancel_right₀ (Complex.exp (c * x)) hc]
    apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
    simpa only [mul_one] using ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x
rw :
  Complex.exp (c * (↑b : ℂ)) / c - Complex.exp (c * (↑a : ℂ)) / c =
    (Complex.exp (c * (↑b : ℂ)) - Complex.exp (c * (↑a : ℂ))) / c
rw₁ : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ Complex.exp (c * (↑x : ℂ))) [[a, b]]
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * (↑x : ℂ)) = (Complex.exp (c * (↑b : ℂ)) - Complex.exp (c * (↑a : ℂ))) / c

Tactic:
rw [integral_deriv_eq_sub' _ (funext fun x => (D x).deriv) fun x _ => (D x).differentiableAt]

Premises used: HasDerivAt.differentiableAt, HasDerivAt.deriv, funext, intervalIntegral.integral_deriv_eq_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x
⊢ Complex.exp (c * (↑b : ℂ)) / c - Complex.exp (c * (↑a : ℂ)) / c =
    (Complex.exp (c * (↑b : ℂ)) - Complex.exp (c * (↑a : ℂ))) / c

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ Complex.exp (c * (↑x : ℂ))) [[a, b]]

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
simp_rw :
  ∫ (t : ℝ) in -r..r, Complex.exp (Complex.I * (↑t : ℂ)) =
    (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I
⊢ ∫ (t : ℝ) in -r..r, Complex.exp ((↑t : ℂ) * Complex.I) =
    (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I

Tactic:
simp_rw [mul_comm _ Complex.I]

Premises used: mul_comm, Complex.I