awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c : ℝ
⊢ c * ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
smul_integral_comp_mul_right f c

Premises used: intervalIntegral.smul_integral_comp_mul_right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c : ℝ
⊢ c * ∫ (x : ℝ) in a..b, f (c * x) = ∫ (x : ℝ) in c * a..c * b, f x

Tactic:
smul_integral_comp_mul_left f c

Premises used: intervalIntegral.smul_integral_comp_mul_left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c : ℝ
⊢ c⁻¹ * ∫ (x : ℝ) in a..b, f (x / c) = ∫ (x : ℝ) in a / c..b / c, f x

Tactic:
inv_smul_integral_comp_div f c

Premises used: intervalIntegral.inv_smul_integral_comp_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c d : ℝ
⊢ c * ∫ (x : ℝ) in a..b, f (c * x + d) = ∫ (x : ℝ) in c * a + d..c * b + d, f x

Tactic:
smul_integral_comp_mul_add f c d

Premises used: intervalIntegral.smul_integral_comp_mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c d : ℝ
⊢ c * ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x

Tactic:
smul_integral_comp_add_mul f c d

Premises used: intervalIntegral.smul_integral_comp_add_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c d : ℝ
⊢ c⁻¹ * ∫ (x : ℝ) in a..b, f (x / c + d) = ∫ (x : ℝ) in a / c + d..b / c + d, f x

Tactic:
inv_smul_integral_comp_div_add f c d

Premises used: intervalIntegral.inv_smul_integral_comp_div_add
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c d : ℝ
⊢ c⁻¹ * ∫ (x : ℝ) in a..b, f (d + x / c) = ∫ (x : ℝ) in d + a / c..d + b / c, f x

Tactic:
inv_smul_integral_comp_add_div f c d

Premises used: intervalIntegral.inv_smul_integral_comp_add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c d : ℝ
⊢ c * ∫ (x : ℝ) in a..b, f (c * x - d) = ∫ (x : ℝ) in c * a - d..c * b - d, f x

Tactic:
smul_integral_comp_mul_sub f c d

Premises used: intervalIntegral.smul_integral_comp_mul_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c d : ℝ
⊢ c * ∫ (x : ℝ) in a..b, f (d - c * x) = ∫ (x : ℝ) in d - c * b..d - c * a, f x

Tactic:
smul_integral_comp_sub_mul f c d

Premises used: intervalIntegral.smul_integral_comp_sub_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c d : ℝ
⊢ c⁻¹ * ∫ (x : ℝ) in a..b, f (x / c - d) = ∫ (x : ℝ) in a / c - d..b / c - d, f x

Tactic:
inv_smul_integral_comp_div_sub f c d

Premises used: intervalIntegral.inv_smul_integral_comp_div_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
c d : ℝ
⊢ c⁻¹ * ∫ (x : ℝ) in a..b, f (d - x / c) = ∫ (x : ℝ) in d - b / c..d - a / c, f x

Tactic:
inv_smul_integral_comp_sub_div f c d

Premises used: intervalIntegral.inv_smul_integral_comp_sub_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
rw : ∫ (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) - (↑a : ℂ) ^ (r + 1)) / (r + 1)

Tactic:
rw [sub_div]

Premises used: sub_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
inl : ∀ (h : -1 < r.re), r + 1 ≠ 0
inr : ∀ (h : r ≠ -1 ∧ 0 ∉ [[a, b]]), r + 1 ≠ 0
⊢ r + 1 ≠ 0

Tactic:
rcases h with h | h
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
apply_fun : (r + 1).re ≠ Complex.re 0
⊢ r + 1 ≠ 0

Tactic:
apply_fun Complex.re

Premises used: Complex.re
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
rw : ¬r.re = -1
⊢ (r + 1).re ≠ Complex.re 0

Tactic:
rw [Complex.add_re, Complex.one_re, Complex.zero_re, Ne, add_eq_zero_iff_eq_neg]

Premises used: Complex.add_re, add_eq_zero_iff_eq_neg, Ne, Complex.zero_re, Complex.one_re
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ ¬r.re = -1

Tactic:
h.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ ¬r.re = -1

Tactic:
exact h.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ¬r + 1 = 0 ∧ 0 ∉ [[a, b]]

Tactic:
rw [Ne, ← add_eq_zero_iff_eq_neg] at h

Premises used: add_eq_zero_iff_eq_neg, Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : ¬r + 1 = 0 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : ¬r + 1 = 0 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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)
neg :
  ∀ (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)

Tactic:
by_cases hab : (0 : ℝ) ∉ [[a, b]]

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : 0 ∉ [[a, b]]
apply : ∀ (x : ℝ) (hx : x ∈ [[a, b]]), HasDerivAt (fun {b : ℝ} ↦ (↑b : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)

Tactic:
apply integral_eq_sub_of_hasDerivAt (fun x hx => ?_)
      (intervalIntegrable_cpow (r := r) <| Or.inr hab)

Premises used: intervalIntegral.intervalIntegrable_cpow, intervalIntegral.integral_eq_sub_of_hasDerivAt, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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

Tactic:
hasDerivAt_ofReal_cpow_const' (ne_of_mem_of_not_mem hx hab) ?_

Premises used: ne_of_mem_of_not_mem, hasDerivAt_ofReal_cpow_const'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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]]
refine : r ≠ -1
⊢ HasDerivAt (fun {b : ℝ} ↦ (↑b : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x

Tactic:
refine hasDerivAt_ofReal_cpow_const' (ne_of_mem_of_not_mem hx hab) ?_

Premises used: ne_of_mem_of_not_mem, hasDerivAt_ofReal_cpow_const'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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]]
contrapose : ∀ (hr : r = -1), r + 1 = 0
⊢ r ≠ -1

Tactic:
contrapose hr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hab : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
hr : r = -1
rwa rwa₁ rwa₂ rwa₃ : r = -1
⊢ r + 1 = 0

Tactic:
rwa [add_eq_zero_iff_eq_neg]

Premises used: add_eq_zero_iff_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
inr : ∀ (hab : 0 ∈ [[a, b]]), r ≠ -1 → 0 ∉ [[a, b]] → -1 < r.re
inl₁ inl₂ : ∀ (hab : 0 ∈ [[a, b]]) (h : -1 < r.re), -1 < r.re
⊢ -1 < r.re

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
⊢ -1 < r.re

Tactic:
replace h : -1 < r.re := by tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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)
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)
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑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]

Premises used: intervalIntegral.integral_add_adjacent_intervals, intervalIntegral.integral_symm, Complex.zero_cpow, intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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)
⊢ -((↑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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
neg : ∀ (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)

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
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
neg₂ : IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ (↑y : ℂ) ^ r) MeasureTheory.volume 0 c
⊢ ∫ (x : ℝ) in 0..c, (↑x : ℂ) ^ r = (↑c : ℂ) ^ (r + 1) / (r + 1) - HPow.hPow (α := ℂ) 0 (r + 1) / (r + 1)

Tactic:
apply integral_eq_sub_of_hasDeriv_right

Premises used: intervalIntegral.integral_eq_sub_of_hasDeriv_right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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]]

Tactic:
((Complex.continuous_ofReal_cpow_const ?_).div_const _).continuousOn

Premises used: Continuous.continuousOn, Continuous.div_const, Complex.continuous_ofReal_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
neg : 0 < (r + 1).re
⊢ ContinuousOn (Y := ℂ) (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) [[0, c]]

Tactic:
refine ((Complex.continuous_ofReal_cpow_const ?_).div_const _).continuousOn

Premises used: Continuous.continuousOn, Continuous.div_const, Complex.continuous_ofReal_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
neg : 0 < r.re + Complex.re 1
neg₁ : 0 < r.re + 1
neg₂ neg₃ neg₄ neg₅ : -1 < r.re
⊢ 0 < (r + 1).re

Tactic:
rwa [Complex.add_re, Complex.one_re, ← neg_lt_iff_pos_add]

Premises used: Complex.add_re, neg_lt_iff_pos_add, Complex.one_re
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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

Tactic:
fun x hx => (hasDerivAt_ofReal_cpow_const' ?_ ?_).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, hasDerivAt_ofReal_cpow_const'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
neg₁ : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (min 0 c) (max 0 c)), r ≠ -1
⊢ ∀ x ∈ Set.Ioo (min 0 c) (max 0 c),
    HasDerivWithinAt (fun (c : ℝ) ↦ (↑c : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (Set.Ioi x) x

Tactic:
refine fun x hx => (hasDerivAt_ofReal_cpow_const' ?_ ?_).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, hasDerivAt_ofReal_cpow_const'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
neg₁ : ∀ (hc : 0 ≤ c), x ≠ 0
⊢ x ≠ 0

Tactic:
rcases le_total c 0 with (hc | hc)

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 ∈ Set.Ioo (min 0 c) 0

Tactic:
rw [max_eq_left hc] at hx

Premises used: max_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
hx₁ : x ∈ Set.Ioo (min 0 c) 0
⊢ c ≤ 0

Tactic:
rw [max_eq_left hc] at hx

Premises used: max_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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) 0
hc : c ≤ 0
⊢ x ≠ 0

Tactic:
hx.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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) 0
hc : c ≤ 0
⊢ x ≠ 0

Tactic:
exact hx.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 ∈ Set.Ioo 0 (max 0 c)

Tactic:
rw [min_eq_left hc] at hx

Premises used: min_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
hx₁ : x ∈ Set.Ioo 0 (max 0 c)
⊢ 0 ≤ c

Tactic:
rw [min_eq_left hc] at hx

Premises used: min_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo 0 (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0

Tactic:
hx.1.ne'

Premises used: LT.lt.ne', And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo 0 (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0

Tactic:
exact hx.1.ne'

Premises used: LT.lt.ne', And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 : ∀ (hr : r = -1), r + 1 = 0
⊢ r ≠ -1

Tactic:
contrapose hr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
neg : HAdd.hAdd (α := ℂ) (-1) 1 = 0
⊢ r + 1 = 0

Tactic:
rw [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ HAdd.hAdd (α := ℂ) (-1) 1 = 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ (↑y : ℂ) ^ r) MeasureTheory.volume 0 c

Tactic:
intervalIntegrable_cpow' h

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ (↑y : ℂ) ^ r) MeasureTheory.volume 0 c

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]]
inl : -1 < r → -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
inr : r ≠ -1 ∧ 0 ∉ [[a, b]] → -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]

Tactic:
cases h
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r
inl : -1 < (↑r : ℂ).re
⊢ -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]

Tactic:
left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h inl inl₁ inl₂ inl₃ : -1 < r
⊢ -1 < (↑r : ℂ).re

Tactic:
rwa [Complex.ofReal_re]

Premises used: Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
inr : (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -1 < (↑r : ℂ).re ∨ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]

Tactic:
right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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]]
inr₃ inr₄ inr₅ inr₆ : ¬r = -1 ∧ 0 ∉ [[a, b]]
⊢ (↑r : ℂ) ≠ -1 ∧ 0 ∉ [[a, b]]

Tactic:
rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]

Premises used: Complex.ofReal_neg, Complex.ofReal_one, Ne, Complex.ofReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -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]
-- 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]]
⊢ ∫ (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'
-- 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 : ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ) = ((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)
⊢ Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re

Tactic:
apply_fun Complex.re at this

Premises used: Complex.re
-- 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
⊢ Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ)) =
    (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re

Tactic:
this
-- 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₁ : ∫ (x : ℝ) in a..b, x ^ r = Complex.re (∫ (x : ℝ) in a..b, (↑x : ℂ) ^ (↑r : ℂ))
h₂ :
  (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = (((↑b : ℂ) ^ ((↑r : ℂ) + 1) - (↑a : ℂ) ^ ((↑r : ℂ) + 1)) / ((↑r : ℂ) + 1)).re
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)

Tactic:
convert! this
-- 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₁ :
  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 : ℂ)) :
        ℝ)
⊢ ∫ (x : ℝ) in a..b, x ^ r = Complex.re (∫ (x : ℝ) in a..b, (↑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]

Premises used: Complex.real_smul, intervalIntegral.intervalIntegral_eq_integral_uIoc, RCLike.re_eq_complex_re, smul_eq_mul, Real.rpow_def, Complex.re_ofReal_mul
-- 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₁ :
  @MeasureTheory.Integrable ℂ _ _ _ measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ))
    (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b))
⊢ 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:
rw [integral_re]

Premises used: integral_re
-- 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
⊢ @MeasureTheory.Integrable ℂ _ _ _ measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ))
    (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b))

Tactic:
intervalIntegrable_iff.mp ?_

Premises used: intervalIntegrable_iff, MeasureTheory.IntegrableOn, Iff.mp
-- 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₁ : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ)) MeasureTheory.volume a b
⊢ @MeasureTheory.Integrable ℂ _ _ _ measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (↑r : ℂ))
    (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b))

Tactic:
refine intervalIntegrable_iff.mp ?_

Premises used: intervalIntegrable_iff, Iff.mp