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

Proof state:
case neg.hderiv.refine_2
a b : ℝ
r : ℂ
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
hr : r = -1
⊢ r + 1 = 0

Tactic:
rw [hr]

Result:
case neg.hderiv.refine_2
a b : ℝ
r : ℂ
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
hr : r = -1
⊢ -1 + 1 = 0

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

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

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

case neg
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)

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

Tactic:
replace h : -1 < r.re := by tauto

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

Proof state:
case neg.hderiv.refine_1.inl
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
hc : c ≤ 0
⊢ x ≠ 0

Tactic:
rw [max_eq_left hc] at hx

Result:
case neg.hderiv.refine_1.inl
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) 0
hc : c ≤ 0
⊢ x ≠ 0

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hab : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
hr : r = -1
⊢ r + 1 = 0

Tactic:
rwa [add_eq_zero_iff_eq_neg]

Result:
no goals

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

Tactic:
contrapose! hr

Result:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hab : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
hr : r = -1
⊢ r + 1 = 0

Proof state:
case inl
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ r + 1 ≠ 0

Tactic:
apply_fun Complex.re

Result:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ (r + 1).re ≠ Complex.re 0

Proof state:
case neg.hcont
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ 0 < (r + 1).re

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

Result:
no goals

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

Tactic:
rw [Ne, ← add_eq_zero_iff_eq_neg] at h

Result:
case inr
a b : ℝ
r : ℂ
h : ¬r + 1 = 0 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0

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

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

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

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
⊢ -1 < r.re

Tactic:
tauto

Result:
no goals

Proof state:
case inr
a b : ℝ
r : ℂ
h : ¬r + 1 = 0 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0

Tactic:
exact h.1

Result:
no goals

Proof state:
case neg.hderiv.refine_1.inr
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
hc : 0 ≤ c
⊢ x ≠ 0

Tactic:
rw [min_eq_left hc] at hx

Result:
case neg.hderiv.refine_1.inr
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo 0 (0 ⊔ c)
hc : 0 ≤ c
⊢ x ≠ 0

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

Result:
no goals

Proof state:
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) - 0 ^ (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]

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

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ (r + 1).re ≠ Complex.re 0

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

Result:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ ¬r.re = -1

Proof state:
case neg.hderiv
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ x ∈ Set.Ioo (0 ⊓ c) (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

Result:
case neg.hderiv.refine_1
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
⊢ x ≠ 0

case neg.hderiv.refine_2
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
⊢ r ≠ -1

Proof state:
case neg.hderiv.refine_1.inr
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo 0 (0 ⊔ c)
hc : 0 ≤ c
⊢ x ≠ 0

Tactic:
exact hx.1.ne'

Result:
no goals

Proof state:
case neg.hderiv.refine_1
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
⊢ x ≠ 0

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

Result:
case neg.hderiv.refine_1.inl
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
hc : c ≤ 0
⊢ x ≠ 0

case neg.hderiv.refine_1.inr
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
hc : 0 ≤ c
⊢ x ≠ 0

Proof state:
case neg.hderiv.refine_2
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
⊢ r ≠ -1

Tactic:
contrapose! hr

Result:
case neg.hderiv.refine_2
a b : ℝ
r : ℂ
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
hr : r = -1
⊢ r + 1 = 0

Proof state:
case neg.hderiv.refine_2
a b : ℝ
r : ℂ
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c)
hr : r = -1
⊢ -1 + 1 = 0

Tactic:
ring

Result:
no goals

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

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

Result:
case neg
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) - 0 ^ (r + 1) / (r + 1)

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ ¬r.re = -1

Tactic:
exact h.ne'

Result:
no goals