-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem intervalIntegrable_cpow {r : ℂ} (h : 0 ≤ r.re ∨ (0 : ℝ) ∉ [[a, b]]) :
    IntervalIntegrable (fun x : ℝ => (x : ℂ) ^ r) μ a b

Proof state:
case neg.inr.refine_2.inl
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c

Tactic:
have : IntervalIntegrable (fun _ => 1 : ℝ → ℝ) μ 0 c := intervalIntegrable_const

Result:
case neg.inr.refine_2.inl
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntervalIntegrable (fun x => 1) μ 0 c
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c

Proof state:
case neg.inr.refine_2
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c

Tactic:
intro c

Result:
case neg.inr.refine_2
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c

Proof state:
case neg.inr.refine_2.inr.h
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ c 0

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc.le]

Result:
case neg.inr.refine_2.inr.h
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioc c 0) μ

Proof state:
case neg.inr.refine_2.inr.h.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Set.Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ IntegrableOn (fun x => ‖Complex.exp (↑π * Complex.I * r)‖) (Set.Ioo c 0) μ

Tactic:
rw [integrableOn_const]

Result:
case neg.inr.refine_2.inr.h.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Set.Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = 0 ∨ μ (Set.Ioo c 0) < ⊤

Proof state:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ ∀ x ∈ Set.Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖

Tactic:
intro x hx

Result:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Set.Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖

Proof state:
case neg.inr.refine_2
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ IntervalIntegrable (fun t => ‖↑t ^ r‖) μ a b

Tactic:
suffices ∀ c : ℝ, IntervalIntegrable (fun x : ℝ => ‖(x : ℂ) ^ r‖) μ 0 c from
  (this a).symm.trans (this b)

Result:
case neg.inr.refine_2
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c

Proof state:
case neg.inr.refine_2.inr.h.left
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) {0} μ

Tactic:
refine integrableOn_singleton_iff.mpr (Or.inr ?_)

Result:
case neg.inr.refine_2.inr.h.left
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ μ {0} < ⊤

Proof state:
case neg.inr.refine_2.inr.h.left
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ μ {0} < ⊤

Tactic:
exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact
  isCompact_singleton

Result:
no goals

Proof state:
case pos
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
h2 : 0 ∉ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b

Tactic:
refine (continuousOn_of_forall_continuousAt fun x hx => ?_).intervalIntegrable

Result:
case pos
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
h2 : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ ContinuousAt (fun x => ↑x ^ r) x

Proof state:
case neg
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b

Tactic:
rcases lt_or_eq_of_le h with (h' | h')

Result:
case neg.inl
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 < r.re
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b

case neg.inr
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b

Proof state:
case neg.inr.refine_2.inr.h
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioc c 0) μ

Tactic:
rw [← Ioo_union_right hc, integrableOn_union, and_comm]

Result:
case neg.inr.refine_2.inr.h
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) {0} μ ∧ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0) μ

Proof state:
case neg.inr.refine_2.inr.h.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0) μ

Tactic:
have : ∀ x : ℝ, x ∈ Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖(x : ℂ) ^ r‖ := by
  intro x hx
  rw [Complex.ofReal_cpow_of_nonpos hx.2.le, norm_mul, ← Complex.ofReal_neg,
    Complex.norm_cpow_eq_rpow_re_of_pos (neg_pos.mpr hx.2), ← h',
    rpow_zero, one_mul]

Result:
case neg.inr.refine_2.inr.h.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Set.Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0) μ

Proof state:
case neg.inr.refine_2.inr
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c

Tactic:
apply IntervalIntegrable.symm

Result:
case neg.inr.refine_2.inr.h
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ c 0

Proof state:
case neg.inr.refine_2.inr.h
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) {0} μ ∧ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0) μ

Tactic:
constructor

Result:
case neg.inr.refine_2.inr.h.left
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) {0} μ

case neg.inr.refine_2.inr.h.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0) μ