awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
rw : t ^ (p - 1) * (1 / (t + 1)) = t ^ (p - 1) * 1 / (t + 1)
rw₁ rw₂ : t ^ (p - 1) * (1 / (t + 1)) = t ^ (p - 1) * (1 / (t + 1))
⊢ t ^ (p - 1) * (1 / (t + 1)) = p.rpowIntegrand₀₁ t 1

Tactic:
rw [rpowIntegrand₀₁_eq_pow_div hp (by linarith) zero_le_one, mul_div_assoc]

Premises used: mul_div_assoc, zero_le_one, Real.rpowIntegrand₀₁_eq_pow_div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
ht : 0 < t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ p.rpowIntegrand₀₁ t x = t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹)

Tactic:
simp [field, rpowIntegrand₀₁]

Premises used: Real.rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
ht : 0 < t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
rw : t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ p / t * (1 - (1 + x * t⁻¹)⁻¹)
⊢ t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹)

Tactic:
rw [Real.rpow_sub_one ht.ne']

Premises used: Real.rpow_sub_one, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
ht : 0 < t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ p / t * (1 - (1 + x * t⁻¹)⁻¹)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
ht : 0 < t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹) = (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x

Tactic:
simp [mul_comm, smul_eq_mul, rpowIntegrand₀₁]

Premises used: Real.rpowIntegrand₀₁, mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
ht : 0 < t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
calc : p.rpowIntegrand₀₁ t x = t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹)
calc₁ : t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹)
calc₂ : t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹) = (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x
⊢ p.rpowIntegrand₀₁ t x = (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x

Tactic:
calc _ = t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) := by simp [field, rpowIntegrand₀₁]
    _ = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹) := by
          rw [Real.rpow_sub_one ht.ne']
          ring
    _ = _ := by simp [mul_comm, smul_eq_mul, rpowIntegrand₀₁]

Premises used: HMul.hMul, HSub.hSub, Inv.inv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioc 0 1)
    volume

Tactic:
IntegrableOn.congr_set_ae (t := Ioo 0 1) ?_ (Filter.EventuallyEq.symm Ioo_ae_eq_Ioc)

Premises used: MeasureTheory.Ioo_ae_eq_Ioc, MeasureTheory.IntegrableOn.congr_set_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
refine :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1)
    volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioc 0 1)
    volume

Tactic:
refine IntegrableOn.congr_set_ae (t := Ioo 0 1) ?_ (Filter.EventuallyEq.symm Ioo_ae_eq_Ioc)

Premises used: MeasureTheory.Ioo_ae_eq_Ioc, MeasureTheory.IntegrableOn.congr_set_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1)
    volume

Tactic:
⟨?meas, ?finite⟩

Premises used: MeasureTheory.Integrable, MeasureTheory.IntegrableOn, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
refine :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))
refine₁ :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1)
    volume

Tactic:
refine ⟨?meas, ?finite⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))

Tactic:
ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioo

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
refine : ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioo

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1)

Tactic:
ContinuousOn.mono (continuousOn_rpowIntegrand₀₁ hp hx) Ioo_subset_Ioi_self

Premises used: ContinuousOn.mono, Real.continuousOn_rpowIntegrand₀₁, Set.Ioo_subset_Ioi_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1)

Tactic:
exact ContinuousOn.mono (continuousOn_rpowIntegrand₀₁ hp hx) Ioo_subset_Ioi_self

Premises used: ContinuousOn.mono, Real.continuousOn_rpowIntegrand₀₁, Set.Ioo_subset_Ioi_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))

Tactic:
case meas =>
    refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioo
    exact ContinuousOn.mono (continuousOn_rpowIntegrand₀₁ hp hx) Ioo_subset_Ioi_self

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioo, ContinuousOn.mono, Real.continuousOn_rpowIntegrand₀₁, Set.Ioo_subset_Ioi_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))

Tactic:
HasFiniteIntegral.mono' (g := fun t => t ^ (p - 1)) ?finitebound ?ae_le

Premises used: MeasureTheory.HasFiniteIntegral.mono'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
refine :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1))
    (Measure.restrict volume (Ioo 0 1))
refine₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) a
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))

Tactic:
refine HasFiniteIntegral.mono' (g := fun t => t ^ (p - 1)) ?finitebound ?ae_le

Premises used: MeasureTheory.HasFiniteIntegral.mono'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
hf : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1)) (Measure.restrict volume (Ioo 0 1))
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1))
    (Measure.restrict volume (Ioo 0 1))

Tactic:
apply Integrable.hasFiniteIntegral

Premises used: MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ 0 < p ∧ p < 1

Tactic:
rw [Set.mem_Ioo] at hp

Premises used: Set.mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
hp₁ : 0 < p ∧ p < 1
⊢ 0 ≤ x

Tactic:
rw [Set.mem_Ioo] at hp

Premises used: Set.mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
hf : -1 < p - 1
hf₁ : LT.lt (α := ℝ) 0 1
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1)) (Measure.restrict volume (Ioo 0 1))

Tactic:
rw [← IntegrableOn, intervalIntegral.integrableOn_Ioo_rpow_iff]

Premises used: intervalIntegral.integrableOn_Ioo_rpow_iff, MeasureTheory.IntegrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
linarith : p - 1 ≤ -1 → 0 - p + (p - 1 - -1) = 0
⊢ -1 < p - 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
⊢ LT.lt (α := ℝ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
⊢ LT.lt (α := ℝ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1))
    (Measure.restrict volume (Ioo 0 1))

Tactic:
case finitebound =>
      apply Integrable.hasFiniteIntegral
      rw [Set.mem_Ioo] at hp
      rw [← IntegrableOn, intervalIntegral.integrableOn_Ioo_rpow_iff]
      · linarith
      · exact zero_lt_one

Premises used: Set.mem_Ioo, intervalIntegral.integrableOn_Ioo_rpow_iff, MeasureTheory.IntegrableOn, zero_lt_one, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) a

Tactic:
ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
refine :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t), ‖p.rpowIntegrand₀₁ t x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) a

Tactic:
refine ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
rw : p.rpowIntegrand₀₁ t x ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t
⊢ ‖p.rpowIntegrand₀₁ t x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t

Tactic:
rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht.1) hx)]

Premises used: le_of_lt, Real.rpowIntegrand₀₁_nonneg, And.left, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
⊢ p.rpowIntegrand₀₁ t x ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t

Tactic:
rpowIntegrand₀₁_le_rpow_sub_one hp (le_of_lt ht.1) hx

Premises used: le_of_lt, And.left, Real.rpowIntegrand₀₁_le_rpow_sub_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
⊢ p.rpowIntegrand₀₁ t x ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t

Tactic:
exact rpowIntegrand₀₁_le_rpow_sub_one hp (le_of_lt ht.1) hx

Premises used: le_of_lt, And.left, Real.rpowIntegrand₀₁_le_rpow_sub_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
case : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t), ‖p.rpowIntegrand₀₁ t x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t
case₁ : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t), p.rpowIntegrand₀₁ t x ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) a

Tactic:
case ae_le =>
      refine ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht.1) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_one hp (le_of_lt ht.1) hx

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
case :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1))
    (Measure.restrict volume (Ioo 0 1))
case₁ case₂ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) a
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))

Tactic:
case finite =>
    refine HasFiniteIntegral.mono' (g := fun t => t ^ (p - 1)) ?finitebound ?ae_le
    case finitebound =>
      apply Integrable.hasFiniteIntegral
      rw [Set.mem_Ioo] at hp
      rw [← IntegrableOn, intervalIntegral.integrableOn_Ioo_rpow_iff]
      · linarith
      · exact zero_lt_one
    case ae_le =>
      refine ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht.1) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_one hp (le_of_lt ht.1) hx

Premises used: Set.mem_Ioo, MeasureTheory.HasFiniteIntegral.mono', intervalIntegral.integrableOn_Ioo_rpow_iff, MeasureTheory.ae_restrict_of_forall_mem, MeasureTheory.IntegrableOn, zero_lt_one, measurableSet_Ioo, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
rw :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Ioc 0 1 ∪ Ioi 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 0) volume

Tactic:
rw [← Set.Ioc_union_Ioi_eq_Ioi zero_le_one]

Premises used: Set.Ioc_union_Ioi_eq_Ioi, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Ioc 0 1 ∪ Ioi 1) volume

Tactic:
IntegrableOn.union (integrableOn_rpowIntegrand₀₁_Ioc hp hx)
    (integrableOn_rpowIntegrand₀₁_Ioi_one hp hx)

Premises used: _private.0.Real.integrableOn_rpowIntegrand₀₁_Ioi_one, MeasureTheory.IntegrableOn.union, _private.0.Real.integrableOn_rpowIntegrand₀₁_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Ioc 0 1 ∪ Ioi 1) volume

Tactic:
exact IntegrableOn.union (integrableOn_rpowIntegrand₀₁_Ioc hp hx)
    (integrableOn_rpowIntegrand₀₁_Ioi_one hp hx)

Premises used: _private.0.Real.integrableOn_rpowIntegrand₀₁_Ioi_one, MeasureTheory.IntegrableOn.union, _private.0.Real.integrableOn_rpowIntegrand₀₁_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ici 0) volume

Tactic:
integrableOn_rpowIntegrand₀₁_Ioi hp hx |>.congr_set_ae Ioi_ae_eq_Ici.symm

Premises used: Real.integrableOn_rpowIntegrand₀₁_Ioi, MeasureTheory.Ioi_ae_eq_Ici, MeasureTheory.IntegrableOn.congr_set_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
inl :
  ∀ (hx : LE.le (α := ℝ) 0 0),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 0) =
      HPow.hPow (α := ℝ) 0 p *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1
inr :
  ∀ (hx : 0 < x),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t x) =
      x ^ p *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1

Tactic:
obtain (rfl | hx) := hx.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : LE.le (α := ℝ) 0 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 0) =
    HPow.hPow (α := ℝ) 0 p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1

Tactic:
simp [rpowIntegrand₀₁, Real.zero_rpow hp.1.ne']

Premises used: Real.zero_rpow, Real.rpowIntegrand₀₁, LT.lt.ne', And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ x * x_1) (Ici 0)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
hft : Tendsto (β := ℝ) (fun (x_1 : ℝ) ↦ x * x_1) atTop atTop
hff' : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x_1 → HasDerivWithinAt (fun (x_2 : ℝ) ↦ x * x_2) x (Ioi x_1) x_1
hg_cont : ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ((fun (x_1 : ℝ) ↦ x * x_1) '' Ioi 0)
hg1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    ((fun (x_1 : ℝ) ↦ x * x_1) '' Ici 0) volume
hg2 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x_1 : ℝ) ↦ ((fun (x_2 : ℝ) ↦ p.rpowIntegrand₀₁ x_2 x) ∘ fun (x_2 : ℝ) ↦ x * x_2) x_1 * x) (Ici 0) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1

Tactic:
rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this

Premises used: MulZeroClass.mul_zero, MeasureTheory.integral_comp_mul_deriv_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ) ↦ x * x_1) atTop atTop

Tactic:
tendsto_id.const_mul_atTop hx

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_id
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
⊢ Tendsto (β := ℝ) (fun (x_1 : ℝ) ↦ x * x_1) atTop atTop

Tactic:
exact tendsto_id.const_mul_atTop hx

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_id
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx_1 : 0 ≤ x
hx : 0 < x
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun (x_1 : ℝ) ↦ x * x_1) t * x) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1
⊢ ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x_1 → HasDerivWithinAt (fun (x_2 : ℝ) ↦ x * x_2) x (Ioi x_1) x_1

Tactic:
simpa using fun t _ ↦ hasDerivWithinAt_id t (Ioi t) |>.const_mul x

Premises used: Set.Ioi, HasDerivWithinAt.const_mul, hasDerivWithinAt_id