-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_rpow {r : ℝ} (h : -1 < r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]) :
    ∫ x in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)

Proof state:
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'

Result:
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)

Proof state:
case h.e'_2
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r ∂MeasureTheory.volume =
    (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r ∂MeasureTheory.volume).re

Tactic:
have : Complex.re = RCLike.re := rfl

Result:
case h.e'_2
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r ∂MeasureTheory.volume =
    (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r ∂MeasureTheory.volume).re

Proof state:
case h.e'_2
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r ∂MeasureTheory.volume =
    (if a ≤ b then 1 else -1) * ∫ (x : ℝ) in Ι a b, RCLike.re (↑x ^ ↑r) ∂MeasureTheory.volume

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3
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).re = ((↑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 : ℝ) : ℂ))]

Result:
case h.e'_3
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).re = ((↑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

Proof state:
case h.e'_2
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ∫ (x : ℝ) in a..b, x ^ r = (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re

Tactic:
simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.re_ofReal_mul]

Result:
case h.e'_2
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r ∂MeasureTheory.volume =
    (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r ∂MeasureTheory.volume).re

Proof state:
case h.e'_2.inl
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
h' : -1 < (↑r).re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b

Tactic:
exact intervalIntegrable_cpow' h'

Result:
no goals

Proof state:
case h.e'_2.inr
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
h' : ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b

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

Result:
no goals

Proof state:
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)

Tactic:
apply_fun Complex.re at this

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

Proof state:
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).re = ((↑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

Result:
case h.e'_2
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ∫ (x : ℝ) in a..b, x ^ r = (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re

case h.e'_3
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).re = ((↑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

Proof state:
case inr
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]

Tactic:
right

Result:
case inr.h
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]

Proof state:
case inr.h
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]

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

Result:
no goals

Proof state:
case h.e'_3
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).re = ((↑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:
simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.re_ofReal_mul, Complex.sub_re]

Result:
case h.e'_3
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * ((↑b ^ ↑(r + 1)).re - (↑a ^ ↑(r + 1)).re)

Proof state:
case inl.h
a b r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re

Tactic:
rwa [Complex.ofReal_re]

Result:
no goals

Proof state:
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]

Tactic:
cases h

Result:
case inl
a b r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]

case inr
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]

Proof state:
case h.e'_3
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * ((↑b ^ ↑(r + 1)).re - (↑a ^ ↑(r + 1)).re)

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_2
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
⊢ MeasureTheory.Integrable (fun x => ↑x ^ ↑r) (MeasureTheory.volume.restrict (Ι a b))

Tactic:
refine intervalIntegrable_iff.mp ?_

Result:
case h.e'_2
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).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ⇑RCLike.re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b