awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
by_cases : ∀ (hx_zero : x = 0), p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have by_cases₁ : ∀ (hx_zero : ¬x = 0), p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
Tactic: by_cases hx_zero : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have simp : 0 ≤ t ^ (p - 1)
Tactic: simp only [rpowIntegrand₀₁, hx_zero, add_zero, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have rw : t ^ (p - 1) * x / (t + x) = t ^ (p - 1) * x / (t + x)
Tactic: rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
have hdb : x ≤ t + x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ x ≤ t + x
have linarith : t + x < x → 0 - t + (t + x - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1
have e_a : x / x = 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have _ : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
Tactic: calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
_ : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have _₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
Tactic: calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
_ : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
_₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have _₂ : t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)
Tactic: calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
_ : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
_₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
_₂ : t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have _₃ : t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1
Tactic: calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
_ : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
_₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
_₂ : t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)
_₃ : t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have _₄ : t ^ (p - 1) * 1 = t ^ (p - 1)
Tactic: calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have case : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
Tactic: case neg =>
    calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
case : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have case₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
Tactic: case neg =>
    calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
case : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
case₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have case₂ : t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)
Tactic: case neg =>
    calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
case : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
case₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
case₂ : t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have case₃ : t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1
Tactic: case neg =>
    calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
case : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
case₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
case₂ : t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)
case₃ : t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
have case₄ : t ^ (p - 1) * 1 = t ^ (p - 1)
Tactic: case neg =>
    calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
⊢ 1 / 2 * t ^ (p - 2) = t ^ (p - 1) * (1 / 2 * 1 / t)
have this : p - 2 = p - 1 - 1
Tactic: have : p - 2 = p - 1 - 1 := by ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 0 < t
have linarith : t ≤ 0 → -1 + (1 - t) + (t - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 1 / 2 * t ^ (p - 2) = t ^ (p - 1) * (1 / 2 * 1 / t)
have rw : 1 / 2 * (t ^ (p - 1) / t) = t ^ (p - 1) * (1 / 2 * 1 / t)
Tactic: rw [this, Real.rpow_sub (by linarith), Real.rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
⊢ t ^ (p - 1) * (1 / 2 * 1 / t) ≤ t ^ (p - 1) * (1 / (t + 1))
have hbc : 1 / 2 * 1 / t ≤ 1 / (t + 1)
Tactic: gcongr t ^ (p - 1) * ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
⊢ 1 / 2 * 1 / t ≤ 1 / (t + 1)
have hbc : t + 1 ≤ 2 * t
Tactic: rw [mul_div_assoc, one_div_mul_one_div,
              one_div_le_one_div (by positivity) (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
⊢ t + 1 ≤ 2 * t
have linarith : 2 * t < t + 1 → 1 - t + (2 * t - (t + 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
⊢ 0 ≤ t
have linarith : t < 0 → -1 + (1 - t) + (t - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
⊢ t ^ (p - 1) * (1 / (t + 1)) = p.rpowIntegrand₀₁ t 1
have rw : t ^ (p - 1) * (1 / (t + 1)) = t ^ (p - 1) * 1 / (t + 1)
Tactic: rw [rpowIntegrand₀₁_eq_pow_div hp (by linarith) zero_le_one, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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)
⊢ t ^ (p - 1) * (1 / (t + 1)) = p.rpowIntegrand₀₁ t 1
have rw₁ : t ^ (p - 1) * (1 / (t + 1)) = t ^ (p - 1) * (1 / (t + 1))
Tactic: rw [rpowIntegrand₀₁_eq_pow_div hp (by linarith) zero_le_one, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
ht : 0 < t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹)
have rw : t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ p / t * (1 - (1 + x * t⁻¹)⁻¹)
Tactic: rw [Real.rpow_sub_one ht.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
ht : 0 < t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ p.rpowIntegrand₀₁ t x = (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x
have calc : p.rpowIntegrand₀₁ t x = t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹)
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₀₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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⁻¹)⁻¹)
⊢ p.rpowIntegrand₀₁ t x = (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x
have calc₁ : t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹)
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₀₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
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⁻¹)⁻¹)
⊢ p.rpowIntegrand₀₁ t x = (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x
have calc₂ : t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹) = (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₀₁]
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioc 0 1)
    volume
have refine : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1) volume
Tactic: refine IntegrableOn.congr_set_ae (t := Ioo 0 1) ?_ (Filter.EventuallyEq.symm Ioo_ae_eq_Ioc)
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1)
    volume
have refine : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
  (Measure.restrict volume (Ioo 0 1))
Tactic: refine ⟨?meas, ?finite⟩
-- 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
refine :
  AEStronglyMeasurable (β := ℝ) (m₀ := 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
have refine₁ : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
  (Measure.restrict volume (Ioo 0 1))
Tactic: refine ⟨?meas, ?finite⟩
-- 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
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))
have refine : ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1)
Tactic: refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioo
-- 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
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))
have refine : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1)) (Measure.restrict volume (Ioo 0 1))
Tactic: refine HasFiniteIntegral.mono' (g := fun t => t ^ (p - 1)) ?finitebound ?ae_le
-- 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
refine :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1))
    (Measure.restrict volume (Ioo 0 1))
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))
have refine₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) a
Tactic: refine HasFiniteIntegral.mono' (g := fun t => t ^ (p - 1)) ?finitebound ?ae_le
-- 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
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1))
    (Measure.restrict volume (Ioo 0 1))
have hf : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1)) (Measure.restrict volume (Ioo 0 1))
Tactic: apply Integrable.hasFiniteIntegral
-- 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
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1)) (Measure.restrict volume (Ioo 0 1))
have hp₁ : 0 < p ∧ p < 1
Tactic: rw [Set.mem_Ioo] at hp
Cleared hypotheses: hp, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1)) (Measure.restrict volume (Ioo 0 1))
have hf : -1 < p - 1
Tactic: rw [← IntegrableOn, intervalIntegral.integrableOn_Ioo_rpow_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
hf : -1 < p - 1
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1)) (Measure.restrict volume (Ioo 0 1))
have hf₁ : LT.lt (α := ℝ) 0 1
Tactic: rw [← IntegrableOn, intervalIntegral.integrableOn_Ioo_rpow_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
⊢ -1 < p - 1
have linarith : p - 1 ≤ -1 → 0 - p + (p - 1 - -1) = 0
Tactic: linarith
-- 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
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) a
have refine : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t), ‖p.rpowIntegrand₀₁ t x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t
Tactic: refine ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_
-- 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
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
⊢ ‖p.rpowIntegrand₀₁ t x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t
have rw : 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)]
-- 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
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) a
have case : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t), ‖p.rpowIntegrand₀₁ t x‖ ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t
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
-- 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
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
have case₁ : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t), p.rpowIntegrand₀₁ t x ≤ (fun (t : ℝ) ↦ t ^ (p - 1)) t
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
-- 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
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioo 0 1))
have case : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ t ^ (p - 1)) (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