awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 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)
have 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)
Tactic: rcases eq_or_lt_of_le' hx with hx_zero | _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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)
⊢ 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)
have 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)
Tactic: rcases eq_or_lt_of_le' hx with hx_zero | _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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)
have hp₁ : 0 < p ∧ p < 1
Tactic: push _ ∈ _ at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hx : 0 ≤ x
hx_zero : x = 0
hp : 0 < p ∧ p < 1
⊢ p ≠ 0
have linarith : p = 0 → 0 - p + (p - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 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)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 0 < x
this :
  Ne (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    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)
have rw : x ^ p =
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹ *
    (x ^ p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)
Tactic: rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 0 < x
this :
  Ne (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    0
rw :
  x ^ p =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹ *
      (x ^ p *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 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)
have rw₁ : x ^ p =
  (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 1)⁻¹
Tactic: rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 0 < x
this :
  Ne (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    0
rw :
  x ^ p =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹ *
      (x ^ p *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)
rw₁ :
  x ^ p =
    (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 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)
have rw₂ : x ^ p =
  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 1)⁻¹
Tactic: rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 0 < x
this :
  Ne (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    0
rw :
  x ^ p =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹ *
      (x ^ p *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)
rw₁ :
  x ^ p =
    (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 1)⁻¹
rw₂ :
  x ^ p =
    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 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)
have rw₃ : x ^ p = x ^ p * 1
Tactic: rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 0 < x
this :
  Ne (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      p.rpowIntegrand₀₁ t 1)
    0
rw :
  x ^ p =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹ *
      (x ^ p *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)
rw₁ :
  x ^ p =
    (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 1)⁻¹
rw₂ :
  x ^ p =
    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 1)⁻¹
rw₃ : x ^ p = x ^ 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)
have rw₄ : x ^ p = x ^ p
Tactic: rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h : 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)
have case : ∀
  (this :
    Ne (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)
      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 inr =>
    have : ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 ≠ 0 :=
      ne_of_gt <| integral_rpowIntegrand₀₁_one_pos hp
    rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
have rw : LE.le (α := ℝ) 0
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    p.rpowIntegrand₀₁ t 1)
Tactic: rw [inv_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
⊢ ∃ (μ : Measure ℝ),
    ∀ (x : ℝ),
      Membership.mem (γ := Set ℝ) (Ici 0) x →
        IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x) (Ioi 0) μ ∧
          x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂μ
have refine_1 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
  IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x) (Ioi 0) (HSMul.hSMul (β := Measure ℝ) C volume)
Tactic: refine ⟨C • volume, fun x hx => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
refine_1 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
    IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x) (Ioi 0) (HSMul.hSMul (β := Measure ℝ) C volume)
⊢ ∃ (μ : Measure ℝ),
    ∀ (x : ℝ),
      Membership.mem (γ := Set ℝ) (Ici 0) x →
        IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x) (Ioi 0) μ ∧
          x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂μ
have refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
  x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C volume
Tactic: refine ⟨C • volume, fun x hx => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x) ((HSMul.hSMul (β := Measure ℝ) C volume).restrict (Ioi 0))
have refine_1 : Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
  (HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0)))
Tactic: rw [Measure.restrict_smul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C volume
have refine_2 : x ^ p = ∫ (t : ℝ), p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0))
Tactic: simp_rw [Measure.restrict_smul, integral_smul_nnreal_measure, rpow_eq_const_mul_integral hp hx,
      NNReal.smul_def, C, NNReal.coe_mk, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
refine_2 : x ^ p = ∫ (t : ℝ), p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0))
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C volume
have refine_2₁ : x ^ p =
  HSMul.hSMul (β := ℝ) C
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
Tactic: simp_rw [Measure.restrict_smul, integral_smul_nnreal_measure, rpow_eq_const_mul_integral hp hx,
      NNReal.smul_def, C, NNReal.coe_mk, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
refine_2 : x ^ p = ∫ (t : ℝ), p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0))
refine_2₁ :
  x ^ p =
    HSMul.hSMul (β := ℝ) C
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C volume
have refine_2₂ : 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) =
  HSMul.hSMul (β := ℝ) C
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
Tactic: simp_rw [Measure.restrict_smul, integral_smul_nnreal_measure, rpow_eq_const_mul_integral hp hx,
      NNReal.smul_def, C, NNReal.coe_mk, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
refine_2 : x ^ p = ∫ (t : ℝ), p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0))
refine_2₁ :
  x ^ p =
    HSMul.hSMul (β := ℝ) C
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
refine_2₂ :
  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) =
    HSMul.hSMul (β := ℝ) C
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C volume
have refine_2₃ : 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) =
  HSMul.hSMul (β := ℝ) (↑C : ℝ)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
Tactic: simp_rw [Measure.restrict_smul, integral_smul_nnreal_measure, rpow_eq_const_mul_integral hp hx,
      NNReal.smul_def, C, NNReal.coe_mk, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
refine_2 : x ^ p = ∫ (t : ℝ), p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0))
refine_2₁ :
  x ^ p =
    HSMul.hSMul (β := ℝ) C
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
refine_2₂ :
  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) =
    HSMul.hSMul (β := ℝ) C
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
refine_2₃ :
  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) =
    HSMul.hSMul (β := ℝ) (↑C : ℝ)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
refine_2₄ :
  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) =
    HSMul.hSMul (β := ℝ)
      (↑(NNReal.mk
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
                p.rpowIntegrand₀₁ t 1)⁻¹
            ⋯) :
        ℝ)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C volume
have refine_2₅ : 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) =
  HSMul.hSMul (α := ℝ) (β := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
Tactic: simp_rw [Measure.restrict_smul, integral_smul_nnreal_measure, rpow_eq_const_mul_integral hp hx,
      NNReal.smul_def, C, NNReal.coe_mk, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ 0 ≤ p.rpowIntegrand₁₂ t x
have pos : ∀ (ht' : 0 < t), 0 ≤ p.rpowIntegrand₁₂ t x
Tactic: by_cases ht' : 0 < t
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : 1 < p
ht : 0 ≤ t
hx : 0 ≤ x
pos : ∀ (ht' : 0 < t), 0 ≤ p.rpowIntegrand₁₂ t x
⊢ 0 ≤ p.rpowIntegrand₁₂ t x
have neg : ∀ (ht' : ¬0 < t), 0 ≤ p.rpowIntegrand₁₂ t x
Tactic: by_cases ht' : 0 < t