-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem intervalIntegrable_rpow' {r : ℝ} (h : -1 < r) :
    IntervalIntegrable (fun x => x ^ r) volume a b

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ContinuousOn (fun x => x ^ (r + 1) / (r + 1)) (Set.Icc 0 c)

Tactic:
refine (continuousOn_id.rpow_const ?_).div_const _

Result:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ∀ x ∈ Set.Icc 0 c, id x ≠ 0 ∨ 0 ≤ r + 1

Proof state:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c

Tactic:
rw [IntervalIntegrable.iff_comp_neg, neg_zero]

Result:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x => (-x) ^ r) volume 0 (-c)

Proof state:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ (cos (r * π) • fun x => x ^ r) x = (fun x => (-x) ^ r) x

Tactic:
simp only [Pi.smul_apply, Algebra.id.smul_eq_mul, log_neg_eq_log, mul_comm,
  rpow_def_of_pos hx.1, rpow_def_of_neg (by linarith [hx.1] : -x < 0)]

Result:
no goals

Proof state:
case h
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Set.Icc 0 c
⊢ 0 ≤ r + 1

Tactic:
linarith

Result:
no goals

Proof state:
a b r : ℝ
h : -1 < r
⊢ IntervalIntegrable (fun x => x ^ r) volume a b

Tactic:
suffices ∀ c : ℝ, IntervalIntegrable (fun x => x ^ r) volume 0 c by
  exact IntervalIntegrable.trans (this a).symm (this b)

Result:
a b r : ℝ
h : -1 < r
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => x ^ r) volume 0 c

Proof state:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
x : ℝ
hx : x ∈ Ι 0 (-c)
⊢ 0 ≤ -c

Tactic:
linarith

Result:
no goals

Proof state:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ 0 ≤ -c

Tactic:
linarith

Result:
no goals

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ 0 ≤ x ^ r

Tactic:
apply rpow_nonneg hx.1.le

Result:
no goals

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ r + 1 ≠ 0

Tactic:
linarith

Result:
no goals

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun x => x ^ r) (Set.Ioc 0 c) volume

Tactic:
have hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun x : ℝ => x ^ (r + 1) / (r + 1)) (x ^ r) x := by
  intro x hx
  convert (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1
  field_simp [(by linarith : r + 1 ≠ 0)]

Result:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ IntegrableOn (fun x => x ^ r) (Set.Ioc 0 c) volume

Proof state:
case h.e'_9
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ x ^ r = (r + 1) * x ^ (r + 1 - 1) / (r + 1)

Tactic:
field_simp [(by linarith : r + 1 ≠ 0)]

Result:
no goals

Proof state:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x => (-x) ^ r) volume 0 (-c)

Tactic:
have m := (this (-c) (by linarith)).smul (cos (r * π))

Result:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntervalIntegrable (cos (r * π) • fun x => x ^ r) volume 0 (-c)
⊢ IntervalIntegrable (fun x => (-x) ^ r) volume 0 (-c)

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ∀ x ∈ Set.Icc 0 c, id x ≠ 0 ∨ 0 ≤ r + 1

Tactic:
intro x _

Result:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Set.Icc 0 c
⊢ id x ≠ 0 ∨ 0 ≤ r + 1

Proof state:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c

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

Result:
case inl
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c

case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ∀ x ∈ Set.Ioo 0 c, 0 ≤ x ^ r

Tactic:
intro x hx

Result:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ 0 ≤ x ^ r

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x

Tactic:
intro x hx

Result:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ IntegrableOn (fun x => x ^ r) (Set.Ioc 0 c) volume

Tactic:
apply integrableOn_deriv_of_nonneg _ hderiv

Result:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ∀ x ∈ Set.Ioo 0 c, 0 ≤ x ^ r

a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ContinuousOn (fun x => x ^ (r + 1) / (r + 1)) (Set.Icc 0 c)

Proof state:
a b r : ℝ
h : -1 < r
⊢ ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c

Tactic:
intro c hc

Result:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c

Proof state:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
x : ℝ
hx : x ∈ Ι 0 (-c)
⊢ (cos (r * π) • fun x => x ^ r) x = (fun x => (-x) ^ r) x

Tactic:
rw [uIoc_of_le (by linarith : 0 ≤ -c)] at hx

Result:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ (cos (r * π) • fun x => x ^ r) x = (fun x => (-x) ^ r) x

Proof state:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ -x < 0

Tactic:
linarith [hx.1]

Result:
no goals

Proof state:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntervalIntegrable (cos (r * π) • fun x => x ^ r) volume 0 (-c)
⊢ IntervalIntegrable (fun x => (-x) ^ r) volume 0 (-c)

Tactic:
rw [intervalIntegrable_iff] at m ⊢

Result:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
⊢ IntegrableOn (fun x => (-x) ^ r) (Ι 0 (-c)) volume