-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integrableOn_rpow_mul_exp_neg_rpow {p s : ℝ} (hs : -1 < s) (hp : 1 ≤ p) :
    IntegrableOn (fun x : ℝ => x ^ s * exp (- x ^ p)) (Ioi 0)

Proof state:
case inl.left.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x : ℝ
a✝ : x ∈ Icc 0 1
⊢ ContinuousWithinAt (fun x => rexp (-x ^ p)) (Icc 0 1) x

Tactic:
change ContinuousWithinAt ((fun x => exp (- x)) ∘ (fun x => x ^ p)) (Icc 0 1) x

Result:
case inl.left.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x : ℝ
a✝ : x ∈ Icc 0 1
⊢ ContinuousWithinAt ((fun x => rexp (-x)) ∘ fun x => x ^ p) (Icc 0 1) x

Proof state:
case inl.left.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x : ℝ
a✝ : x ∈ Icc 0 1
⊢ ContinuousWithinAt ((fun x => rexp (-x)) ∘ fun x => x ^ p) (Icc 0 1) x

Tactic:
refine ContinuousAt.comp_continuousWithinAt (h_exp _) ?_

Result:
case inl.left.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x : ℝ
a✝ : x ∈ Icc 0 1
⊢ ContinuousWithinAt (fun x => x ^ p) (Icc 0 1) x

Proof state:
case inl.right.refine_1
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
x : ℝ
hx : x ∈ Ici 1
⊢ ContinuousWithinAt (fun x => rexp (-x ^ p)) (Ici 1) x

Tactic:
change ContinuousWithinAt ((fun x => exp (- x)) ∘ (fun x => x ^ p)) (Ici 1) x

Result:
case inl.right.refine_1
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
x : ℝ
hx : x ∈ Ici 1
⊢ ContinuousWithinAt ((fun x => rexp (-x)) ∘ fun x => x ^ p) (Ici 1) x

Proof state:
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x✝ r✝ : ℝ
hx : x✝ ∈ Ici 1
⊢ id x✝ ≠ 0

Tactic:
exact ne_of_gt (lt_of_lt_of_le zero_lt_one hx)

Result:
no goals

Proof state:
case inl.left
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Icc 0 1) volume

Tactic:
refine IntegrableOn.mul_continuousOn ?_ ?_ isCompact_Icc

Result:
case inl.left.refine_1
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s) (Icc 0 1) volume

case inl.left.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ ContinuousOn (fun x => rexp (-x ^ p)) (Icc 0 1)

Proof state:
case inr
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 = p
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Tactic:
simp_rw [← hp, Real.rpow_one]

Result:
case inr
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 = p
⊢ IntegrableOn (fun x => x ^ s * rexp (-x)) (Ioi 0) volume

Proof state:
case inl.left.refine_1
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s) (Icc 0 1) volume

Tactic:
refine (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_

Result:
case inl.left.refine_1
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntervalIntegrable (fun x => x ^ s) volume 0 1

Proof state:
case h.e'_6.h
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 = p
x✝ : ℝ
⊢ x✝ ^ s * rexp (-x✝) = rexp (-x✝) * x✝ ^ (s + 1 - 1)

Tactic:
rw [add_sub_cancel_right, mul_comm]

Result:
no goals

Proof state:
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x✝ r✝ : ℝ
hx : x✝ ∈ Ici 1
⊢ ContinuousWithinAt (fun x => x ^ r✝) (Ici 1) x✝

Tactic:
refine continuousWithinAt_id.rpow_const (Or.inl ?_)

Result:
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x✝ r✝ : ℝ
hx : x✝ ∈ Ici 1
⊢ id x✝ ≠ 0