awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) ((fun (x_1 : ℝ) ↦ x * x_1) '' Ioi 0)

Tactic:
simpa [Set.image_mul_left_Ioi hx] using continuousOn_rpowIntegrand₀₁ hp hx.le

Premises used: Set.image_mul_left_Ioi, LT.lt.le, Real.continuousOn_rpowIntegrand₀₁
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    ((fun (x_1 : ℝ) ↦ x * x_1) '' Ici 0) volume

Tactic:
simpa [Set.image_mul_left_Ici hx] using integrableOn_rpowIntegrand₀₁_Ici hp hx.le

Premises used: LT.lt.le, Set.image_mul_left_Ici, Real.integrableOn_rpowIntegrand₀₁_Ici
-- 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
hg2 : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ici 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ (x * x_1) x * x)
    (Ici 0) volume

Tactic:
rw [integrableOn_congr_fun (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le) measurableSet_Ici]

Premises used: MeasureTheory.integrableOn_congr_fun, Real.rpowIntegrand₀₁_apply_mul_eqOn_Ici, LT.lt.le, measurableSet_Ici
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ici 0) volume

Tactic:
Integrable.mul_const (integrableOn_rpowIntegrand₀₁_Ici hp zero_le_one) _

Premises used: MeasureTheory.IntegrableOn, zero_le_one, MeasureTheory.Integrable.mul_const, Real.integrableOn_rpowIntegrand₀₁_Ici
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ici 0) volume

Tactic:
exact Integrable.mul_const (integrableOn_rpowIntegrand₀₁_Ici hp zero_le_one) _

Premises used: zero_le_one, MeasureTheory.Integrable.mul_const, Real.integrableOn_rpowIntegrand₀₁_Ici
-- 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
inr :
  (@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
⊢ (@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:
suffices ∫ t in Ioi 0, ((rpowIntegrand₀₁ p · x) ∘ (x * ·)) t * x =
      x ^ p * (∫ t in Ioi 0, rpowIntegrand₀₁ p t 1) by
    rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this
    · exact tendsto_id.const_mul_atTop hx
    · simpa using fun t _ ↦ hasDerivWithinAt_id t (Ioi t) |>.const_mul x
    · simpa [Set.image_mul_left_Ioi hx] using continuousOn_rpowIntegrand₀₁ hp hx.le
    · simpa [Set.image_mul_left_Ici hx] using integrableOn_rpowIntegrand₀₁_Ici hp hx.le
    · simp only [Function.comp]
      rw [integrableOn_congr_fun (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le) measurableSet_Ici]
      exact Integrable.mul_const (integrableOn_rpowIntegrand₀₁_Ici hp zero_le_one) _
-- 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
⊢ EqOn (β := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)

Tactic:
have heqOn : EqOn (fun t => rpowIntegrand₀₁ p (x * t) x * x)
      (fun t => (rpowIntegrand₀₁ p t 1) * x ^ p) (Ioi 0) :=
    EqOn.mono Ioi_subset_Ici_self (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le)
-- 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
heqOn :
  EqOn (β := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
inr :
  HSMul.hSMul (α := ℝ)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1)
      (x ^ p) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        p.rpowIntegrand₀₁ x 1
⊢ (@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

Tactic:
simp only [Function.comp, setIntegral_congr_fun measurableSet_Ioi heqOn,
    ← smul_eq_mul (b := x ^ p), integral_smul_const]

Premises used: integral_smul_const, Function.comp, measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun, HPow.hPow, smul_eq_mul
-- 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
heqOn :
  EqOn (β := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
inr :
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1) * x ^ p =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        p.rpowIntegrand₀₁ x 1
inr₁ inr₂ :
  (x ^ p * @integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        p.rpowIntegrand₀₁ x 1
⊢ HSMul.hSMul (α := ℝ)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ p.rpowIntegrand₀₁ x 1)
      (x ^ p) =
    x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        p.rpowIntegrand₀₁ x 1

Tactic:
rw [smul_eq_mul, mul_comm]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
rw : -1 / 2 / (p - 1) = 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1)
⊢ -1 / (2 * (p - 1)) = 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1)

Tactic:
rw [← div_div]

Premises used: div_div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ -1 / 2 / (p - 1) = 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1)

Tactic:
simp [neg_div]

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

Tactic:
push _ ∈ _ at hp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : 0 < p ∧ p < 1
linarith : -1 ≤ p - 2 → p - 1 + (-1 - (p - 2)) = 0
⊢ p - 2 < -1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : 0 < p ∧ p < 1
rw : 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1) = 1 / 2 * (-HPow.hPow (α := ℝ) 1 (p - 2 + 1) / (p - 2 + 1))
⊢ 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)

Tactic:
rw [integral_const_mul, integral_Ioi_rpow_of_lt (by linarith) zero_lt_one]

Premises used: MeasureTheory.integral_const_mul, integral_Ioi_rpow_of_lt, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 1 / 2 * -HPow.hPow (α := ℝ) 1 (p - 1) / (p - 1) = 1 / 2 * (-HPow.hPow (α := ℝ) 1 (p - 2 + 1) / (p - 2 + 1))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      1 / 2 * t ^ (p - 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)

Tactic:
setIntegral_mono_on ?_ ?_ measurableSet_Ioi ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
refine_1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)) (Ioi 1) volume
refine_2 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1) (Ioi 1) volume
refine_3 : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 1) x → 1 / 2 * x ^ (p - 2) ≤ p.rpowIntegrand₀₁ x 1
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      1 / 2 * t ^ (p - 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)

Tactic:
refine setIntegral_mono_on ?_ ?_ measurableSet_Ioi ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)) (Ioi 1) volume

Tactic:
Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.IntegrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
refine_1 :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 2)) (Measure.restrict volume (Ioi 1))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ 1 / 2 * t ^ (p - 2)) (Ioi 1) volume

Tactic:
refine Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : 0 < p ∧ p < 1
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 2)) (Measure.restrict volume (Ioi 1))

Tactic:
exact integrableOn_Ioi_rpow_of_lt (by linarith) zero_lt_one

Premises used: integrableOn_Ioi_rpow_of_lt, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1) (Ioi 1) volume

Tactic:
integrableOn_rpowIntegrand₀₁_Ioi_one hp zero_le_one

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

Tactic:
exact integrableOn_rpowIntegrand₀₁_Ioi_one hp zero_le_one

Premises used: _private.0.Real.integrableOn_rpowIntegrand₀₁_Ioi_one, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 1) x → 1 / 2 * x ^ (p - 2) ≤ p.rpowIntegrand₀₁ x 1

Tactic:
fun t ht => rpowIntegrand₀₁_one_ge_rpow_sub_two hp (le_of_lt ht)

Premises used: le_of_lt, Real.rpowIntegrand₀₁_one_ge_rpow_sub_two
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 1) x → 1 / 2 * x ^ (p - 2) ≤ p.rpowIntegrand₀₁ x 1

Tactic:
exact fun t ht => rpowIntegrand₀₁_one_ge_rpow_sub_two hp (le_of_lt ht)

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

Tactic:
setIntegral_mono_set (integrableOn_rpowIntegrand₀₁_Ioi hp zero_le_one) ?_ ?_

Premises used: Real.integrableOn_rpowIntegrand₀₁_Ioi, MeasureTheory.setIntegral_mono_set, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
refine_1 :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1
refine_2 : Ioi 1 ≤ᶠ[ae (F := Measure ℝ) volume] Ioi 0
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 1)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)

Tactic:
refine setIntegral_mono_set (integrableOn_rpowIntegrand₀₁_Ioi hp zero_le_one) ?_ ?_

Premises used: Real.integrableOn_rpowIntegrand₀₁_Ioi, MeasureTheory.setIntegral_mono_set, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1

Tactic:
ae_restrict_of_forall_mem measurableSet_Ioi fun t ht => ?_

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioi, Filter.EventuallyLE
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
refine_1 :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t), LE.le (α := ℝ) (0 t) ((fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1) t)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1

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

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ LE.le (α := ℝ) (0 t) ((fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1) t)

Tactic:
rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht) zero_le_one

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

Tactic:
exact rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht) zero_le_one

Premises used: le_of_lt, Real.rpowIntegrand₀₁_nonneg, zero_le_one, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ Ioi 1 ≤ᶠ[ae (F := Measure ℝ) volume] Ioi 0

Tactic:
.of_forall <| Set.Ioi_subset_Ioi zero_le_one

Premises used: Filter.Eventually.of_forall, zero_le_one, Set.Ioi_subset_Ioi, Filter.EventuallyLE
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ Ioi 1 ≤ᶠ[ae (F := Measure ℝ) volume] Ioi 0

Tactic:
exact .of_forall <| Set.Ioi_subset_Ioi zero_le_one

Premises used: zero_le_one, Set.Ioi_subset_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
rw : 2 * (p - 1) < 0
⊢ 0 < -1 / (2 * (p - 1))

Tactic:
rw [neg_div, neg_pos, one_div_neg]

Premises used: neg_div, neg_pos, one_div_neg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : 0 < p ∧ p < 1
linarith : 0 ≤ 2 * (p - 1) → 2 * (p - 1) + (0 - 2 * (p - 1)) = 0
linarith₁ : 0 ≤ 2 * (p - 1) → GT.gt (α := ℝ) 2 0
⊢ 2 * (p - 1) < 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
rcases :
  ∀ (hx_zero : x = 0),
    x ^ p =
      HMul.hMul (α := ℝ)
        (@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)
rcases₁ :
  0 < x →
    x ^ p =
      HMul.hMul (α := ℝ)
        (@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 =
    HMul.hMul (α := ℝ)
      (@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)

Tactic:
rcases eq_or_lt_of_le' hx with hx_zero | _

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

Tactic:
push _ ∈ _ at hp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hx : 0 ≤ x
hx_zero : x = 0
hp : 0 < p ∧ p < 1
linarith : p = 0 → 0 - p + (p - 0) = 0
⊢ p ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hx : 0 ≤ x
hx_zero : x = 0
hp : 0 < p ∧ p < 1
⊢ x ^ p =
    HMul.hMul (α := ℝ)
      (@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)

Tactic:
simp [hx_zero, Real.zero_rpow (by linarith)]

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
hx_zero : x = 0
⊢ x ^ p =
    HMul.hMul (α := ℝ)
      (@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)

Tactic:
case inl =>
    push _ ∈ _ at hp
    simp [hx_zero, Real.zero_rpow (by linarith)]

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 0 < x
⊢ Ne (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    0

Tactic:
have : ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 ≠ 0 :=
      ne_of_gt <| integral_rpowIntegrand₀₁_one_pos hp