awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (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 t x : ℝ
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
hp : 0 < p ∧ p < 1
⊢ p - 1 ≠ 0
have linarith : p - 1 = 0 → p - 1 + -(p - 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t x : ℝ
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
hp : 0 < p ∧ p < 1
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have hp₂ : p - 1 ≠ 0
Tactic: have hp₂ : p - 1 ≠ 0 := by 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
ht' : t = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have case : ∀ (hp : 0 < p ∧ p < 1), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
Tactic: case pos =>
    push _ ∈ _ at hp
    have hp₂ : p - 1 ≠ 0 := by linarith
    simp [rpowIntegrand₀₁, ht', hp.1.ne', hp₂]
Cleared hypotheses: hp
-- 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
ht' : t = 0
case : ∀ (hp : 0 < p ∧ p < 1), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have case₁ : ∀ (hp : 0 < p ∧ p < 1) (hp₂ : p - 1 ≠ 0), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
Tactic: case pos =>
    push _ ∈ _ at hp
    have hp₂ : p - 1 ≠ 0 := by linarith
    simp [rpowIntegrand₀₁, ht', hp.1.ne', hp₂]
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ (x * t) x = p.rpowIntegrand₀₁ t 1 * x ^ (p - 1)
have hxt : 0 ≤ x * t
Tactic: have hxt : 0 ≤ x * t := by positivity
-- 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
hxt : 0 ≤ x * t
⊢ p.rpowIntegrand₀₁ (x * t) x = p.rpowIntegrand₀₁ t 1 * x ^ (p - 1)
have rw : (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
Tactic: rw [rpowIntegrand₀₁_eq_pow_div hp hxt hx, rpowIntegrand₀₁_eq_pow_div hp ht zero_le_one]
-- 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
hxt : 0 ≤ x * t
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
have by_cases : ∀ (hx_zero : x = 0), (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (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
hxt : 0 ≤ x * t
by_cases : ∀ (hx_zero : x = 0), (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
have by_cases₁ : ∀ (hx_zero : ¬x = 0), (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x)))
have rw : (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))
Tactic: rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
rw : (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x)))
have rw₁ : (x * t) ^ (p - 1) * (x / (x * t + x)) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))
Tactic: rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
rw : (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))
rw₁ : (x * t) ^ (p - 1) * (x / (x * t + x)) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x)))
have rw₂ : x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x)) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))
Tactic: rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))
have this : x * t + x = x * (t + 1)
Tactic: have : x * t + x = x * (t + 1) := by ring
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
this : x * t + x = x * (t + 1)
⊢ x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))
have rw : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
Tactic: rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
this : x * t + x = x * (t + 1)
rw : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
⊢ x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))
have rw₁ : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
Tactic: rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
this : x * t + x = x * (t + 1)
rw : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₁ : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
⊢ x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))
have rw₂ : x ^ (p - 1) * (t ^ (p - 1) * (x / x * (1 / (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
Tactic: rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
this : x * t + x = x * (t + 1)
rw : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₁ : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₂ : x ^ (p - 1) * (t ^ (p - 1) * (x / x * (1 / (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
⊢ x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))
have rw₃ : x ^ (p - 1) * (t ^ (p - 1) * (1 * (1 / (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
Tactic: rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
this : x * t + x = x * (t + 1)
rw : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₁ : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₂ : x ^ (p - 1) * (t ^ (p - 1) * (x / x * (1 / (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₃ : x ^ (p - 1) * (t ^ (p - 1) * (1 * (1 / (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
⊢ x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))
have rw₄ : x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
Tactic: rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
have rw : t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
Tactic: rw [mul_comm]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
have calc : (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x)))
Tactic: calc _ = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) := by
              rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
      _ = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) := by
              have : x * t + x = x * (t + 1) := by ring
              rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
      _ = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) := by rw [mul_comm]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
calc : (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x)))
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
have calc₁ : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))
Tactic: calc _ = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) := by
              rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
      _ = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) := by
              have : x * t + x = x * (t + 1) := by ring
              rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
      _ = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) := by rw [mul_comm]
-- 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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
calc : (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x)))
calc₁ : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
have calc₂ : x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
Tactic: calc _ = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) := by
              rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
      _ = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) := by
              have : x * t + x = x * (t + 1) := by ring
              rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
      _ = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) := by rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
have hp₁ : 0 < p ∧ p < 1
Tactic: rw [mem_Ioo] at hp
Cleared hypotheses: hp, ht, hx, hxt, hx_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : 0 < p ∧ p < 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
⊢ p - 1 ≠ 0
have linarith : p - 1 = 0 → p - 1 + -(p - 1 - 0) = 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
hxt : 0 ≤ x * t
hx_zero : x = 0
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
have case : ∀ (hp : 0 < p ∧ p < 1) (ht : 0 ≤ t) (hx : 0 ≤ x) (hxt : 0 ≤ x * t) (hx_zero : x = 0),
  (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
Tactic: case pos =>
    rw [mem_Ioo] at hp
    simp [hx_zero, Real.zero_rpow (by linarith : p - 1 ≠ 0)]
Cleared hypotheses: hp, ht, hx, hxt, hx_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
⊢ p.rpowIntegrand₀₁ (x * t) x * x = p.rpowIntegrand₀₁ t 1 * x ^ p
have simp : p.rpowIntegrand₀₁ t 1 * (x ^ (p - 1) * x) = p.rpowIntegrand₀₁ t 1 * x ^ p
Tactic: simp only [rpowIntegrand₀₁_apply_mul hp ht hx, mul_assoc]
-- 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
⊢ p.rpowIntegrand₀₁ t 1 * (x ^ (p - 1) * x) = p.rpowIntegrand₀₁ t 1 * x ^ p
have e_a : x ^ (p - 1) * x = x ^ p
Tactic: congr
-- 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
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 0)
have refine : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (p - 1) * x / (t + x)) (Ioi 0)
Tactic: refine ContinuousOn.congr ?_ <| rpowIntegrand₀₁_eqOn_pow_div hp hx
-- 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
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (p - 1) * x / (t + x)) (Ioi 0)
have h₀ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (p - 1)) (Ioi 0)
Tactic: have h₀ : ContinuousOn (· ^ (p - 1) : ℝ → ℝ) (Ioi 0) := .rpow_const (by fun_prop) <|
    fun t ht => .inl ht.ne'
-- 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₀ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (p - 1)) (Ioi 0)
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (p - 1) * x / (t + x)) (Ioi 0)
have funProp : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x_1 → x_1 + x ≠ 0
Tactic: fun_prop (disch := grind -abstractProof)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
have by_cases : ∀ (h : x = 0), p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
by_cases : ∀ (h : x = 0), p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
have by_cases₁ : ∀ (h : ¬x = 0), p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
h : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
have hx₁ : 0 ≤ x
Tactic: simp only [rpowIntegrand₀₁, mem_Ici] at hx h ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
h : ¬x = 0
hx : 0 ≤ x
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) ≤ t ^ p * (t⁻¹ - (t + y)⁻¹)
have ha : 0 ≤ t ^ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
h : ¬x = 0
hx : 0 ≤ x
ha : 0 ≤ t ^ p
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) ≤ t ^ p * (t⁻¹ - (t + y)⁻¹)
have hbc : 0 < t + x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
h : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
have hx₁ : 0 ≤ x
Tactic: case neg =>
    simp only [rpowIntegrand₀₁, mem_Ici] at hx h ⊢
    gcongr
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (Function.uncurry p.rpowIntegrand₀₁) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have refine_1 : ContinuousOn g (SProd.sprod (α := Set ℝ) (Ioi 0) s)
Tactic: refine ContinuousOn.congr (f := g) ?_ fun q => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
refine_1 : ContinuousOn g (SProd.sprod (α := Set ℝ) (Ioi 0) s)
⊢ ContinuousOn (Function.uncurry p.rpowIntegrand₀₁) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have refine_2 : ∀ q ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, Function.uncurry p.rpowIntegrand₀₁ q = g q
Tactic: refine ContinuousOn.congr (f := g) ?_ fun q => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have refine_1 : ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
Tactic: refine ContinuousOn.mul ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
refine_1 : ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have refine_1₁ : ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ (q.1 + q.2)⁻¹) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
Tactic: refine ContinuousOn.mul ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
have refine_1 : ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1)) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
Tactic: refine ContinuousOn.mul ?_ (by fun_prop)
-- 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
⊢ 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 (le_of_lt 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
⊢ t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / t
have hdb : t ≤ 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
⊢ t ≤ t + x
have linarith : t + x < t → 0 - x + (t + x - t) = 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
⊢ t ^ (p - 1) / t * x = t ^ (p - 2) * x
have e_a : t ^ (p - 1) / t = t ^ (p - 2)
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
⊢ t ^ (p - 1) / t = t ^ (p - 2)
have e_a : t ^ (p - 1 - 1) = t ^ (p - 2)
Tactic: rw [← Real.rpow_sub_one (by positivity)]
-- 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
⊢ t ^ (p - 1 - 1) = t ^ (p - 2)
have e_a : p - 1 - 1 = p - 2
Tactic: congr 1
-- 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
⊢ 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