awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = (((↑b : ℂ) ^ (↑(r + 1) : ℂ) - (↑a : ℂ) ^ (↑(r + 1) : ℂ)) / (↑(r + 1) : ℂ)).re
have h₄ : (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * (((↑b : ℂ) ^ (↑(r + 1) : ℂ)).re - ((↑a : ℂ) ^ (↑(r + 1) : ℂ)).re)
Tactic: simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.re_ofReal_mul, Complex.sub_re, rpow_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have h₁ : LT.lt (α := ℝ) (-1) (↑n : ℝ) ∨ Ne (α := ℝ) (↑n : ℝ) (-1) ∧ 0 ∉ [[a, b]]
Tactic: replace h : -1 < (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] := mod_cast h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
⊢ (@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
have 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
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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
⊢ (@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
have 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
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ 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)
have 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)
Tactic: rw [uIoc_of_le hab, ← integral_of_le hab]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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)
⊢ 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)
have rw₁ : Eq (α := ℝ) (∫ (x : ℝ) in a..b, |x - a| ^ n) (∫ (x : ℝ) in a..b, |x - a| ^ n)
Tactic: rw [uIoc_of_le hab, ← integral_of_le hab]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, |x - a| ^ n) (∫ (x : ℝ) in 0..b - a, x ^ n)
have simp : Eq (α := ℝ) (∫ (x : ℝ) in 0..b - a, |x| ^ n) (∫ (x : ℝ) in 0..b - a, x ^ n)
Tactic: simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..b - a, |x| ^ n) (∫ (x : ℝ) in 0..b - a, x ^ n)
have refine : ∀ (x : ℝ) (hx : x ∈ [[0, b - a]]), 0 ≤ x
Tactic: refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| ?_) rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ [[0, b - a]]
⊢ 0 ≤ x
have hx₁ : x ∈ Set.Icc 0 (b - a)
Tactic: rw [uIcc_of_le (sub_nonneg.2 hab)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
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
have 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)
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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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)
⊢ (@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
have x₁ : Eq (α := ℝ) (∫ (x : ℝ) in a..b, |x - a| ^ n) (∫ (x : ℝ) in 0..b - a, x ^ n)
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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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)
⊢ (@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
have x₂ : ∫ (x : ℝ) in 0..b - a, x ^ 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
hab : b < a
⊢ 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)
have 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)
Tactic: rw [uIoc_of_ge hab.le, ← integral_of_le hab.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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)
⊢ 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)
have rw₁ : Eq (α := ℝ) (∫ (x : ℝ) in b..a, |x - a| ^ n) (∫ (x : ℝ) in b..a, |x - a| ^ n)
Tactic: rw [uIoc_of_ge hab.le, ← integral_of_le hab.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
hab : b < a
⊢ Eq (α := ℝ) (∫ (x : ℝ) in b..a, |x - a| ^ n) (∫ (x : ℝ) in b - a..0, (-x) ^ n)
have simp : Eq (α := ℝ) (∫ (x : ℝ) in b - a..0, |x| ^ n) (∫ (x : ℝ) in b - a..0, (-x) ^ n)
Tactic: simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
hab : b < a
⊢ Eq (α := ℝ) (∫ (x : ℝ) in b - a..0, |x| ^ n) (∫ (x : ℝ) in b - a..0, (-x) ^ n)
have refine : ∀ (x : ℝ) (hx : x ∈ [[b - a, 0]]), x ≤ 0
Tactic: refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| ?_) rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ [[b - a, 0]]
⊢ x ≤ 0
have hx₁ : x ∈ Set.Icc (b - a) 0
Tactic: rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
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
have 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)
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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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)
⊢ (@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
have x₁ : Eq (α := ℝ) (∫ (x : ℝ) in b..a, |x - a| ^ n) (∫ (x : ℝ) in b - a..0, (-x) ^ n)
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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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)
⊢ (@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
have x₂ : ∫ (x : ℝ) in b - a..0, (-x) ^ 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, x = (HPow.hPow (β := ℕ) b 2 - HPow.hPow (β := ℕ) a 2) / 2
have this : ∫ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
h : 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)
have h' : ∀ (x : ℝ) (hx : x ∈ [[a, b]]), x ≠ 0
Tactic: have h' := fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
h : 0 ∉ [[a, b]]
h' : ∀ (x : ℝ) (hx : x ∈ [[a, b]]), x ≠ 0
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)
have rw : log b - log a = 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
h : 0 ∉ [[a, b]]
h' : ∀ (x : ℝ) (hx : x ∈ [[a, b]]), x ≠ 0
rw : log b - log a = log (b / a)
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)
have rw₁ : log b - log a = log b - log 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, rexp x = rexp b - rexp a
have hderiv : deriv rexp = rexp
Tactic: rw [integral_deriv_eq_sub']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
hderiv : deriv rexp = rexp
⊢ ∫ (x : ℝ) in a..b, rexp x = rexp b - rexp a
have hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x
Tactic: rw [integral_deriv_eq_sub']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
hderiv : deriv rexp = rexp
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x
⊢ ∫ (x : ℝ) in a..b, rexp x = rexp b - rexp a
have hcont : ContinuousOn rexp [[a, b]]
Tactic: rw [integral_deriv_eq_sub']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
| HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x
have f : fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
f : fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c
| HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x
have f' : Complex.exp (c * (↑x : ℂ))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
f : fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c
f' : Complex.exp (c * (↑x : ℂ))
| HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x
have x₁ : x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x
have rw : HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ)) * c / c) x
Tactic: rw [← mul_div_cancel_right₀ (Complex.exp (c * x)) hc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ)) * c / c) x
have apply : HasDerivAt (fun (x : ℝ) ↦ c * (↑x : ℂ)) c x
Tactic: apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * (↑x : ℂ)) = (Complex.exp (c * (↑b : ℂ)) - Complex.exp (c * (↑a : ℂ))) / c
have D : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ Complex.exp (c * (↑y : ℂ)) / c) (Complex.exp (c * (↑x : ℂ))) x
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * (↑x : ℂ)) = (Complex.exp (c * (↑b : ℂ)) - Complex.exp (c * (↑a : ℂ))) / c
have rw : Complex.exp (c * (↑b : ℂ)) / c - Complex.exp (c * (↑a : ℂ)) / c =
  (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * (↑x : ℂ)) = (Complex.exp (c * (↑b : ℂ)) - Complex.exp (c * (↑a : ℂ))) / c
have rw₁ : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ Complex.exp (c * (↑x : ℂ))) [[a, b]]
Tactic: rw [integral_deriv_eq_sub' _ (funext fun x => (D x).deriv) fun x _ => (D x).differentiableAt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp ((↑t : ℂ) * Complex.I) =
    (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I
have simp_rw : ∫ (t : ℝ) in -r..r, Complex.exp (Complex.I * (↑t : ℂ)) =
  (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I
Tactic: simp_rw [mul_comm _ Complex.I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (Complex.I * (↑t : ℂ)) =
    (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I
have rw : (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * (↑(-r) : ℂ))) / Complex.I =
  (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I
Tactic: rw [integral_exp_mul_complex]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
rw :
  (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * (↑(-r) : ℂ))) / Complex.I =
    (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (Complex.I * (↑t : ℂ)) =
    (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I
have rw₁ : Complex.I ≠ 0
Tactic: rw [integral_exp_mul_complex]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
⊢ (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I = 2 * (↑(sin r) : ℂ)
have simp : -((Complex.sin (↑r : ℂ) * Complex.I - -Complex.sin (↑r : ℂ) * Complex.I) * Complex.I) = 2 * Complex.sin (↑r : ℂ)
Tactic: simp only [mul_comm Complex.I, Complex.exp_mul_I, Complex.cos_neg, Complex.sin_neg,
      add_sub_add_left_eq_sub, Complex.div_I, Complex.ofReal_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
⊢ -((Complex.sin (↑r : ℂ) * Complex.I - -Complex.sin (↑r : ℂ) * Complex.I) * Complex.I) = 2 * Complex.sin (↑r : ℂ)
have rw : -(Complex.sin (↑r : ℂ) * (Complex.I * Complex.I) - -Complex.sin (↑r : ℂ) * (Complex.I * Complex.I)) =
  Complex.sin (↑r : ℂ) + Complex.sin (↑r : ℂ)
Tactic: rw [sub_mul, mul_assoc, mul_assoc, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp ((↑t : ℂ) * Complex.I) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
have rw : 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
Tactic: rw [integral_exp_mul_I_eq_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
⊢ 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
have pos : ∀ (hr : r = 0), 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
pos : ∀ (hr : r = 0), 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
⊢ 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
have neg : ∀ (hr : ¬r = 0), 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
hr : ¬r = 0
⊢ 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
have neg : 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sin r / r) : ℂ)
Tactic: rw [sinc_of_ne_zero hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
r : ℝ
hr : ¬r = 0
⊢ 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sin r / r) : ℂ)
have neg : 2 * sin r = 2 * r * (sin r / r)
Tactic: norm_cast