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.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0
have inl : ∀ (h : -1 < r.re), r + 1 ≠ 0
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
inl : ∀ (h : -1 < r.re), r + 1 ≠ 0
⊢ r + 1 ≠ 0
have inr : ∀ (h : r ≠ -1 ∧ 0 ∉ [[a, b]]), r + 1 ≠ 0
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ r + 1 ≠ 0
have apply_fun : (r + 1).re ≠ Complex.re 0
Tactic: apply_fun Complex.re
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ (r + 1).re ≠ Complex.re 0
have rw : ¬r.re = -1
Tactic: rw [Complex.add_re, Complex.one_re, Complex.zero_re, Ne, add_eq_zero_iff_eq_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0
have h₁ : ¬r + 1 = 0 ∧ 0 ∉ [[a, b]]
Tactic: rw [Ne, ← add_eq_zero_iff_eq_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
have hr : r + 1 ≠ 0
Tactic: have hr : r + 1 ≠ 0 := by
    rcases h with h | h
    · apply_fun Complex.re
      rw [Complex.add_re, Complex.one_re, Complex.zero_re, Ne, add_eq_zero_iff_eq_neg]
      exact h.ne'
    · rw [Ne, ← add_eq_zero_iff_eq_neg] at h; exact h.1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
have pos : ∀ (hab : 0 ∉ [[a, b]]), ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
Tactic: by_cases hab : (0 : ℝ) ∉ [[a, b]]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
pos :
  ∀ (hab : 0 ∉ [[a, b]]), ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
have neg : ∀ (hab : ¬0 ∉ [[a, b]]), ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
Tactic: by_cases hab : (0 : ℝ) ∉ [[a, b]]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
have apply : ∀ (x : ℝ) (hx : x ∈ [[a, b]]), HasDerivAt (fun {b : ℝ} ↦ (↑b : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
Tactic: apply integral_eq_sub_of_hasDerivAt (fun x hx => ?_)
      (intervalIntegrable_cpow (r := r) <| Or.inr hab)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b : ℝ} ↦ (↑b : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
have refine : r ≠ -1
Tactic: refine hasDerivAt_ofReal_cpow_const' (ne_of_mem_of_not_mem hx hab) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ r ≠ -1
have contrapose : ∀ (hr : r = -1), r + 1 = 0
Tactic: contrapose hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
⊢ -1 < r.re
have inl : ∀ (hab : 0 ∈ [[a, b]]) (h : -1 < r.re), -1 < r.re
Tactic: tauto
Cleared hypotheses: h, hab
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
inl : ∀ (hab : 0 ∈ [[a, b]]) (h : -1 < r.re), -1 < r.re
⊢ -1 < r.re
have inr : ∀ (hab : 0 ∈ [[a, b]]), r ≠ -1 → 0 ∉ [[a, b]] → -1 < r.re
Tactic: tauto
Cleared hypotheses: h, hab
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
have h₁ : -1 < r.re
Tactic: replace h : -1 < r.re := by tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
this :
  ∀ (c : ℝ), ∫ (x : ℝ) in 0..c, (↑x : ℂ) ^ r = (↑c : ℂ) ^ (r + 1) / (r + 1) - HPow.hPow (α := ℂ) 0 (r + 1) / (r + 1)
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
have rw : -((↑a : ℂ) ^ (r + 1) / (r + 1) - 0 / (r + 1)) + ((↑b : ℂ) ^ (r + 1) / (r + 1) - 0 / (r + 1)) =
  (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
Tactic: rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h)
      (@intervalIntegrable_cpow' 0 b r h), integral_symm, this a, this b, Complex.zero_cpow hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
have neg : ∀ (c : ℝ), ∫ (x : ℝ) in 0..c, (↑x : ℂ) ^ r = (↑c : ℂ) ^ (r + 1) / (r + 1) - HPow.hPow (α := ℂ) 0 (r + 1) / (r + 1)
Tactic: suffices ∀ c : ℝ, (∫ x : ℝ in 0..c, (x : ℂ) ^ r) =
      (c : ℂ) ^ (r + 1) / (r + 1) - (0 : ℂ) ^ (r + 1) / (r + 1) by
    rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h)
      (@intervalIntegrable_cpow' 0 b r h), integral_symm, this a, this b, Complex.zero_cpow hr]
    ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∫ (x : ℝ) in 0..c, (↑x : ℂ) ^ r = (↑c : ℂ) ^ (r + 1) / (r + 1) - HPow.hPow (α := ℂ) 0 (r + 1) / (r + 1)
have neg : ContinuousOn (Y := ℂ) (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) [[0, c]]
Tactic: apply integral_eq_sub_of_hasDeriv_right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
neg : ContinuousOn (Y := ℂ) (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) [[0, c]]
⊢ ∫ (x : ℝ) in 0..c, (↑x : ℂ) ^ r = (↑c : ℂ) ^ (r + 1) / (r + 1) - HPow.hPow (α := ℂ) 0 (r + 1) / (r + 1)
have neg₁ : ∀ x ∈ Set.Ioo (min 0 c) (max 0 c),
  HasDerivWithinAt (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (Set.Ioi x) x
Tactic: apply integral_eq_sub_of_hasDeriv_right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
neg : ContinuousOn (Y := ℂ) (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) [[0, c]]
neg₁ :
  ∀ x ∈ Set.Ioo (min 0 c) (max 0 c),
    HasDerivWithinAt (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (Set.Ioi x) x
⊢ ∫ (x : ℝ) in 0..c, (↑x : ℂ) ^ r = (↑c : ℂ) ^ (r + 1) / (r + 1) - HPow.hPow (α := ℂ) 0 (r + 1) / (r + 1)
have neg₂ : IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ (↑y : ℂ) ^ r) MeasureTheory.volume 0 c
Tactic: apply integral_eq_sub_of_hasDeriv_right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ContinuousOn (Y := ℂ) (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) [[0, c]]
have neg : 0 < (r + 1).re
Tactic: refine ((Complex.continuous_ofReal_cpow_const ?_).div_const _).continuousOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ 0 < (r + 1).re
have neg : 0 < r.re + Complex.re 1
Tactic: rwa [Complex.add_re, Complex.one_re, ← neg_lt_iff_pos_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
neg : 0 < r.re + Complex.re 1
⊢ 0 < (r + 1).re
have neg₁ : 0 < r.re + 1
Tactic: rwa [Complex.add_re, Complex.one_re, ← neg_lt_iff_pos_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ x ∈ Set.Ioo (min 0 c) (max 0 c),
    HasDerivWithinAt (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (Set.Ioi x) x
have neg : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (min 0 c) (max 0 c)), x ≠ 0
Tactic: refine fun x hx => (hasDerivAt_ofReal_cpow_const' ?_ ?_).hasDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
neg : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (min 0 c) (max 0 c)), x ≠ 0
⊢ ∀ x ∈ Set.Ioo (min 0 c) (max 0 c),
    HasDerivWithinAt (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (Set.Ioi x) x
have neg₁ : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (min 0 c) (max 0 c)), r ≠ -1
Tactic: refine fun x hx => (hasDerivAt_ofReal_cpow_const' ?_ ?_).hasDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ x ≠ 0
have neg : ∀ (hc : c ≤ 0), x ≠ 0
Tactic: rcases le_total c 0 with (hc | hc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
neg : ∀ (hc : c ≤ 0), x ≠ 0
⊢ x ≠ 0
have neg₁ : ∀ (hc : 0 ≤ c), x ≠ 0
Tactic: rcases le_total c 0 with (hc | hc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : c ≤ 0
⊢ x ≠ 0
have hx₁ : x ∈ Set.Ioo (min 0 c) 0
Tactic: rw [max_eq_left hc] at hx
Cleared hypotheses: hx, hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0
have hx₁ : x ∈ Set.Ioo 0 (max 0 c)
Tactic: rw [min_eq_left hc] at hx
Cleared hypotheses: hx, hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ r ≠ -1
have neg : ∀ (hr : r = -1), r + 1 = 0
Tactic: contrapose hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hr : r = -1
⊢ r + 1 = 0
have neg : HAdd.hAdd (α := ℂ) (-1) 1 = 0
Tactic: rw [hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
have inl : -1 < r → -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
inl : -1 < r → -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
have inr : r ≠ -1 ∧ 0 ∉ [[a, b]] → -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
⊢ -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
have inl : -1 < (↑r : ℂ).re
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b r : ℝ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
have inr : (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b r : ℝ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
have inr : (↑r : ℂ) ≠ -(↑1 : ℂ) ∧ 0 ∉ [[a, b]]
Tactic: rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b r : ℝ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
inr : (↑r : ℂ) ≠ -(↑1 : ℂ) ∧ 0 ∉ [[a, b]]
⊢ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
have inr₁ : (↑r : ℂ) ≠ (↑(-1) : ℂ) ∧ 0 ∉ [[a, b]]
Tactic: rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b r : ℝ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
inr : (↑r : ℂ) ≠ -(↑1 : ℂ) ∧ 0 ∉ [[a, b]]
inr₁ : (↑r : ℂ) ≠ (↑(-1) : ℂ) ∧ 0 ∉ [[a, b]]
⊢ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
have inr₂ : ¬(↑r : ℂ) = (↑(-1) : ℂ) ∧ 0 ∉ [[a, b]]
Tactic: rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b r : ℝ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
inr : (↑r : ℂ) ≠ -(↑1 : ℂ) ∧ 0 ∉ [[a, b]]
inr₁ : (↑r : ℂ) ≠ (↑(-1) : ℂ) ∧ 0 ∉ [[a, b]]
inr₂ : ¬(↑r : ℂ) = (↑(-1) : ℂ) ∧ 0 ∉ [[a, b]]
⊢ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
have inr₃ : ¬r = -1 ∧ 0 ∉ [[a, b]]
Tactic: rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
have h' : -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
Tactic: have h' : -1 < (r : ℂ).re ∨ (r : ℂ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] := by
    cases h
    · left; rwa [Complex.ofReal_re]
    · right; rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
have this : ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ) = ((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)
Tactic: have :
    (∫ x in a..b, (x : ℂ) ^ (r : ℂ)) = ((b : ℂ) ^ (r + 1 : ℂ) - (a : ℂ) ^ (r + 1 : ℂ)) / (r + 1) :=
    integral_cpow h'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ) = ((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
have this₁ : Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
  (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
Tactic: apply_fun Complex.re at this
Cleared hypotheses: this
-- 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
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
have h₁ : ∫ (x : ℝ) in a..b, x ^ r = Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ))
Tactic: convert! this
-- 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₁ : ∫ (x : ℝ) in a..b, x ^ r = Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ))
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
have h₂ : (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
Tactic: convert! this
-- 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
⊢ ∫ (x : ℝ) in a..b, x ^ r = Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ))
have h₁ : HMul.hMul (α := ℝ) (if a ≤ b then 1 else -1)
    (@MeasureTheory.integral _ _ _ _ measurableSpace (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b))
      fun (x : ℝ) ↦ (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ (↑r : ℂ))) =
  HMul.hMul (α := ℝ) (β := ℝ) (if a ≤ b then 1 else -1 : ℝ)
    ((RCLike.re : (a : ℂ) → ℝ)
        (@MeasureTheory.integral _ _ _ _ measurableSpace (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b))
          fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) :
      ℝ)
Tactic: simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.re_ofReal_mul, rpow_def,
      ← RCLike.re_eq_complex_re, smul_eq_mul]
-- 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
⊢ HMul.hMul (α := ℝ) (if a ≤ b then 1 else -1)
      (@MeasureTheory.integral _ _ _ _ measurableSpace (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b))
        fun (x : ℝ) ↦ (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ (↑r : ℂ))) =
    HMul.hMul (α := ℝ) (β := ℝ) (if a ≤ b then 1 else -1 : ℝ)
      ((RCLike.re : (a : ℂ) → ℝ)
          (@MeasureTheory.integral _ _ _ _ measurableSpace (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b))
            fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) :
        ℝ)
have h₁ : @MeasureTheory.Integrable ℂ _ _ _ measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ))
  (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b))
Tactic: rw [integral_re]
-- 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
⊢ @MeasureTheory.Integrable ℂ _ _ _ measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ))
    (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b))
have h₁ : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b
Tactic: refine intervalIntegrable_iff.mp ?_
-- 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
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b
have h₁ : ∀ (h' : -1 < (↑r : ℂ).re), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b
Tactic: rcases h' with h' | h'
Cleared hypotheses: h'
-- 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₁ : ∀ (h' : -1 < (↑r : ℂ).re), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b
have h₂ : ∀ (h' : (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]),
  IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b
Tactic: rcases h' with h' | h'
Cleared hypotheses: h'
-- 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
⊢ (↑r : ℂ) + 1 = (↑(r + 1) : ℂ)
have push_cast : (↑r : ℂ) + 1 = (↑r : ℂ) + 1
Tactic: push_cast
-- 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
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
have h₁ : (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 : ℝ) : ℂ))]
-- 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
⊢ (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) : ℂ) - (↑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 (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
⊢ (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) : ℂ) - (↑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 (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
⊢ (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) : ℂ) - (↑a : ℂ) ^ (↑(r + 1) : ℂ)).re
Tactic: simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.re_ofReal_mul, Complex.sub_re, rpow_def]