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

Proof state:
case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ EqOn (fun x => x ^ r.re) (fun t => ‖↑t ^ r‖) (Ι 0 c)

Tactic:
intro x hx

Result:
case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ (fun x => x ^ r.re) x = (fun t => ‖↑t ^ r‖) x

Proof state:
case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ x ^ r.re = ‖↑x ^ r‖

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1]

Result:
no goals

Proof state:
case h
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn ?f (Ι 0 c) volume

Tactic:
rw [← intervalIntegrable_iff]

Result:
case h
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable ?m.45094 volume 0 c

a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ℝ → ℝ

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ ContinuousAt (fun x => ↑x ^ r) x

Tactic:
refine (continuousAt_cpow_const (Or.inl ?_)).comp Complex.continuous_ofReal.continuousAt

Result:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 0 < (↑x).re

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ 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.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => ↑x ^ r) volume 0 c

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 0 < x

Tactic:
exact hx.1

Result:
no goals

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun t => ‖↑t ^ r‖) (Ι 0 c) volume

Tactic:
apply IntegrableOn.congr_fun

Result:
case h
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn ?f (Ι 0 c) volume

case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ EqOn ?f (fun t => ‖↑t ^ r‖) (Ι 0 c)

case hs
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ MeasurableSet (Ι 0 c)

case f
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ℝ → ℝ

Proof state:
case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ (fun x => x ^ r.re) x = (fun t => ‖↑t ^ r‖) x

Tactic:
dsimp only

Result:
case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ x ^ r.re = ‖↑x ^ r‖

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

Tactic:
intro c

Result:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
⊢ IntervalIntegrable (fun x => ↑x ^ r) volume 0 c

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re
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.re
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.re
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.re
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.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x => ↑(-x) ^ r) volume 0 (-c)