awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x p : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x

Tactic:
hf.rpow_const hx

Premises used: HasDerivWithinAt.rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x p : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x

Tactic:
exact hf.rpow_const hx

Premises used: HasDerivWithinAt.rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
x p : ℝ
s : Set ℝ
hf : DifferentiableWithinAt ℝ f s x
hx : f x ≠ 0 ∨ 1 ≤ p
hxs : UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun (x : ℝ) ↦ f x ^ p) s x = derivWithin f s x * p * f x ^ (p - 1)

Tactic:
(hf.hasDerivWithinAt.rpow_const hx).derivWithin hxs

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
x p : ℝ
hf : DifferentiableAt ℝ f x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ deriv (fun (x : ℝ) ↦ f x ^ p) x = deriv f x * p * f x ^ (p - 1)

Tactic:
(hf.hasDerivAt.rpow_const hx).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
t : ℝ
ht : 0 < t
rw : deriv (fun (x : ℝ) ↦ x ^ c.re) t = c.re * t ^ (c.re - 1)
rw₁ : (𝓝 t).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ c‖) fun (x : ℝ) ↦ x ^ c.re
⊢ deriv (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ c‖) t = c.re * t ^ (c.re - 1)

Tactic:
rw [EventuallyEq.deriv_eq (f := fun x ↦ x ^ c.re)]

Premises used: Filter.EventuallyEq.deriv_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
t : ℝ
ht : 0 < t
rw rw₁ : c.re * t ^ (c.re - 1) = c.re * t ^ (c.re - 1)
⊢ deriv (fun (x : ℝ) ↦ x ^ c.re) t = c.re * t ^ (c.re - 1)

Tactic:
rw [Real.deriv_rpow_const t]

Premises used: Real.deriv_rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
t : ℝ
ht : 0 < t
h : ∀ (x : ℝ) (hx : 0 < x), ‖(↑x : ℂ) ^ c‖ = x ^ c.re
⊢ (𝓝 t).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ c‖) fun (x : ℝ) ↦ x ^ c.re

Tactic:
filter_upwards [eventually_gt_nhds ht] with x hx

Premises used: eventually_gt_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
t : ℝ
ht : 0 < t
x : ℝ
hx : 0 < x
h h₁ : x ^ c.re = x ^ c.re
⊢ ‖(↑x : ℂ) ^ c‖ = x ^ c.re

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos hx]

Premises used: Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
hp : p ≠ 0
⊢ Eq (α := (x : ℝ) → ℝ) (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ p * x ^ (p - 1)

Tactic:
Real.deriv_rpow_const' p

Premises used: Real.deriv_rpow_const'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
hp : p ≠ 0
⊢ Asymptotics.IsTheta (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ p * x ^ (p - 1)) fun (x : ℝ) ↦ x ^ (p - 1)

Tactic:
Asymptotics.IsTheta.const_mul_left hp Asymptotics.isTheta_rfl

Premises used: Asymptotics.IsTheta.const_mul_left, Asymptotics.isTheta_rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
hp : p ≠ 0
⊢ Asymptotics.IsTheta (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ x ^ (p - 1)

Tactic:
calc deriv (fun (x : ℝ) ↦ x ^ p) = fun x => p * x ^ (p - 1) := Real.deriv_rpow_const' p
    _ =Θ[atTop] fun x ↦ x ^ (p - 1) :=
      Asymptotics.IsTheta.const_mul_left hp Asymptotics.isTheta_rfl

Premises used: Asymptotics.IsTheta.const_mul_left, HMul.hMul, deriv, HSub.hSub, Filter.atTop, Asymptotics.isTheta_rfl, HPow.hPow, Real.deriv_rpow_const', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
rcases :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0) fun (x : ℝ) ↦
    x ^ HSub.hSub (α := ℝ) 0 1
rcases₁ :
  ∀ (hp : p ≠ 0), Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ x ^ (p - 1)
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ x ^ (p - 1)

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0) fun (x : ℝ) ↦
    x ^ HSub.hSub (α := ℝ) 0 1

Tactic:
simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]

Premises used: Asymptotics.isBigO_zero, Real.rpow_neg_one, deriv_const', Real.rpow_zero, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0) fun (x : ℝ) ↦
    x ^ HSub.hSub (α := ℝ) 0 1

Tactic:
case inl =>
    simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]

Premises used: Asymptotics.isBigO_zero, Real.rpow_neg_one, deriv_const', Real.rpow_zero, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
hp : p ≠ 0
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ x ^ (p - 1)

Tactic:
(isTheta_deriv_rpow_const_atTop hp).1

Premises used: isTheta_deriv_rpow_const_atTop, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
hp : p ≠ 0
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ x ^ (p - 1)

Tactic:
exact (isTheta_deriv_rpow_const_atTop hp).1

Premises used: isTheta_deriv_rpow_const_atTop, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
hp : p ≠ 0
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ x ^ (p - 1)

Tactic:
case inr =>
    exact (isTheta_deriv_rpow_const_atTop hp).1

Premises used: isTheta_deriv_rpow_const_atTop, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ a ^ f x) (0 * f x * a ^ (f x - 1) + f' * a ^ f x * Real.log a) s x

Tactic:
(hasDerivWithinAt_const x s a).rpow hf ha

Premises used: HasDerivWithinAt.rpow, hasDerivWithinAt_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : HasDerivWithinAt f f' s x
h : Real.log a * f' * a ^ f x = 0 * f x * a ^ (f x - 1) + f' * a ^ f x * Real.log a
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ a ^ f x) (Real.log a * f' * a ^ f x) s x

Tactic:
convert! (hasDerivWithinAt_const x s a).rpow hf ha using 1

Premises used: HasDerivWithinAt.rpow, hasDerivWithinAt_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : HasDerivWithinAt f f' s x
⊢ Real.log a * f' * a ^ f x = 0 * f x * a ^ (f x - 1) + f' * a ^ f x * Real.log a

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x a : ℝ
ha : 0 < a
hf : HasDerivAt f f' x
rw :
  ∀ (hf : HasDerivWithinAt f f' Set.univ x),
    HasDerivWithinAt (fun (x : ℝ) ↦ a ^ f x) (Real.log a * f' * a ^ f x) Set.univ x
⊢ HasDerivAt (fun (x : ℝ) ↦ a ^ f x) (Real.log a * f' * a ^ f x) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x a : ℝ
ha : 0 < a
hf : HasDerivWithinAt f f' Set.univ x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ a ^ f x) (Real.log a * f' * a ^ f x) Set.univ x

Tactic:
hf.const_rpow ha

Premises used: HasDerivWithinAt.const_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x a : ℝ
ha : 0 < a
hf : HasDerivWithinAt f f' Set.univ x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ a ^ f x) (Real.log a * f' * a ^ f x) Set.univ x

Tactic:
exact hf.const_rpow ha

Premises used: HasDerivWithinAt.const_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
pos : ∀ (hxs : UniqueDiffWithinAt ℝ s x), derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
neg : ∀ (hxs : ¬UniqueDiffWithinAt ℝ s x), derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x

Tactic:
by_cases hxs : UniqueDiffWithinAt ℝ s x

Premises used: Real, UniqueDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x

Tactic:
(hf.hasDerivWithinAt.const_rpow ha).derivWithin hxs

Premises used: HasDerivWithinAt.const_rpow, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x

Tactic:
exact (hf.hasDerivWithinAt.const_rpow ha).derivWithin hxs

Premises used: HasDerivWithinAt.const_rpow, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : ¬UniqueDiffWithinAt ℝ s x
neg : 0 = log a * derivWithin f s x * a ^ f x
neg₁ : 0 = log a * 0 * a ^ f x
neg₂ : 0 = 0 * a ^ f x
neg₃ neg₄ : Eq (α := ℝ) 0 0
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x

Tactic:
rw [derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
x a : ℝ
ha : 0 < a
hf : DifferentiableAt ℝ f x
⊢ deriv (fun (x : ℝ) ↦ a ^ f x) x = log a * deriv f x * a ^ f x

Tactic:
(hf.hasDerivAt.const_rpow ha).deriv

Premises used: HasDerivAt.const_rpow, DifferentiableAt.hasDerivAt, HasDerivAt.deriv
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x a : ℝ
ha : 0 < a
rw : log a * deriv (fun (x : ℝ) ↦ x) x * a ^ x = log a * a ^ x
rw₁ : log a * (fun (x : ℝ) ↦ (1 : ℝ)) x * a ^ x = log a * a ^ x
rw₂ rw₃ : log a * a ^ x = log a * a ^ x
⊢ deriv (fun (x : ℝ) ↦ a ^ x) x = log a * a ^ x

Tactic:
rw [deriv_const_rpow ha differentiableAt_fun_id, deriv_id'', mul_one]

Premises used: deriv_id'', deriv_const_rpow, differentiableAt_fun_id, mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
linarith : p - 1 ≤ -1 → 0 - p + (p - 1 - -1) = 0
⊢ -1 < p - 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ -1 < p - 1

Tactic:
have one_lt_p : -1 < p - 1 := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
x : ℝ
rw : (x ^ (p - 1 + 1) - HPow.hPow (α := ℝ) 0 (p - 1 + 1)) / (p - 1 + 1) = x ^ p / p
⊢ ∫ (t : ℝ) in 0..x, t ^ (p - 1) = x ^ p / p

Tactic:
rw [integral_rpow (Or.inl one_lt_p)]

Premises used: integral_rpow, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
x : ℝ
⊢ (x ^ (p - 1 + 1) - HPow.hPow (α := ℝ) 0 (p - 1 + 1)) / (p - 1 + 1) = x ^ p / p

Tactic:
simp [Real.zero_rpow p_pos.ne.symm]

Premises used: Ne.symm, Real.zero_rpow, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
⊢ ∀ (x : ℝ), ∫ (t : ℝ) in 0..x, t ^ (p - 1) = x ^ p / p

Tactic:
have obs : ∀ x : ℝ, ∫ t : ℝ in 0..x, t ^ (p - 1) = x ^ p / p := by
    intro x
    rw [integral_rpow (Or.inl one_lt_p)]
    simp [Real.zero_rpow p_pos.ne.symm]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
obs : ∀ (x : ℝ), ∫ (t : ℝ) in 0..x, t ^ (p - 1) = x ^ p / p
⊢ let g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1);
  ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p

Tactic:
set g := fun t : ℝ => t ^ (p - 1)

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
h : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) a → 0 ≤ g a
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t

Tactic:
filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]

Premises used: measurableSet_Ioi, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
t : ℝ
t_pos : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ 0 ≤ g t

Tactic:
Real.rpow_nonneg (mem_Ioi.mp t_pos).le (p - 1)

Premises used: HSub.hSub, Set.mem_Ioi, LT.lt.le, Iff.mp, Real.rpow_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
t : ℝ
t_pos : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ 0 ≤ g t

Tactic:
exact Real.rpow_nonneg (mem_Ioi.mp t_pos).le (p - 1)

Premises used: HSub.hSub, Set.mem_Ioi, LT.lt.le, Iff.mp, Real.rpow_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t

Tactic:
have g_nn : ∀ᵐ t ∂volume.restrict (Ioi (0 : ℝ)), 0 ≤ g t := by
    filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]
    intro t t_pos
    exact Real.rpow_nonneg (mem_Ioi.mp t_pos).le (p - 1)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t

Tactic:
have g_intble (t) (ht : 0 < t) : IntervalIntegrable g volume 0 t :=
    intervalIntegral.intervalIntegrable_rpow' one_lt_p
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))

Tactic:
have key := lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
rw :
  ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t) ∂μ
rw₁ : AEMeasurable (β := ENNReal) (fun (ω : α) ↦ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t)) μ
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))

Tactic:
rw [← key, ← lintegral_const_mul'' (ENNReal.ofReal p)]

Premises used: ENNReal.ofReal, MeasureTheory.lintegral_const_mul''
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
simp_rw : ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t) ∂μ

Tactic:
simp_rw [obs]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
simp_rw : AEMeasurable (β := ENNReal) (fun (ω : α) ↦ ENNReal.ofReal (f ω ^ p / p)) μ
⊢ AEMeasurable (β := ENNReal) (fun (ω : α) ↦ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t)) μ

Tactic:
simp_rw [obs]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
e_f : ∀ (ω : α), ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal p * ENNReal.ofReal (f ω ^ p / p)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ

Tactic:
congr with ω
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
ω : α
e_f : ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal (p * (f ω ^ p / p))
e_f₁ e_f₂ : ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal (f ω ^ p)
⊢ ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal p * ENNReal.ofReal (f ω ^ p / p)

Tactic:
rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel₀ (f ω ^ p) p_pos.ne.symm]

Premises used: ENNReal.ofReal_mul, LT.lt.le, Ne.symm, mul_div_cancel₀, HPow.hPow, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ p) μ

Tactic:
have aux := (measurable_const (a := p)).aemeasurable (μ := μ)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
aux : AEMeasurable (β := ℝ) (fun (x : α) ↦ p) μ
⊢ AEMeasurable (β := ENNReal) (fun (ω : α) ↦ ENNReal.ofReal (f ω ^ p / p)) μ

Tactic:
measurable_id.ennreal_ofReal.comp_aemeasurable <| (f_mble.pow aux).div_const p

Premises used: ENNReal.ofNNReal, Measurable.ennreal_ofReal, AEMeasurable.pow, ENNReal.ofReal, measurable_id, AEMeasurable.div_const, WithTop.some, Measurable.comp_aemeasurable
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
aux : AEMeasurable (β := ℝ) (fun (x : α) ↦ p) μ
⊢ AEMeasurable (β := ENNReal) (fun (ω : α) ↦ ENNReal.ofReal (f ω ^ p / p)) μ

Tactic:
exact measurable_id.ennreal_ofReal.comp_aemeasurable <| (f_mble.pow aux).div_const p

Premises used: Measurable.ennreal_ofReal, AEMeasurable.pow, measurable_id, AEMeasurable.div_const, Measurable.comp_aemeasurable