awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
pos : ∀ (hp_zero : p = 0), 0 < x ^ p
⊢ 0 < x ^ p
have neg : ∀ (hp_zero : ¬p = 0), 0 < x ^ p
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p
have hp_zero₁ : p ≠ 0
Tactic: rw [← Ne] at hp_zero
Cleared hypotheses: hp_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < x ^ p
have hp_pos : 0 < p
Tactic: have hp_pos := lt_of_le_of_ne hp_nonneg hp_zero.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 < x ^ p
have neg : HPow.hPow (α := ℝ≥0∞) 0 p < x ^ p
Tactic: rw [← zero_rpow_of_pos hp_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
⊢ 0 < x ^ p
have inl : ∀ (hp_pos : 0 < p), 0 < x ^ p
Tactic: rcases lt_or_ge 0 p with hp_pos | hp_nonpos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
inl : ∀ (hp_pos : 0 < p), 0 < x ^ p
⊢ 0 < x ^ p
have inr : ∀ (hp_nonpos : p ≤ 0), 0 < x ^ p
Tactic: rcases lt_or_ge 0 p with hp_pos | hp_nonpos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ 0 < x ^ p
have inr : x ^ (-p) ≠ ∞
Tactic: rw [← neg_neg p, rpow_neg, ENNReal.inv_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : x < 1
hz : 0 < z
⊢ x ^ z < 1
have lift : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) < 1), (↑x : ℝ≥0∞) ^ z < 1
Tactic: lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx le_top)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : (↑x : ℝ≥0∞) < 1
⊢ (↑x : ℝ≥0∞) ^ z < 1
have hx₁ : x < 1
Tactic: simp only [coe_lt_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1
have lift : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) ≤ 1), (↑x : ℝ≥0∞) ^ z ≤ 1
Tactic: lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx coe_lt_top)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≤ 1
⊢ (↑x : ℝ≥0∞) ^ z ≤ 1
have hx₁ : x ≤ 1
Tactic: simp only [coe_le_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1
have top : ∀ (hx : LT.lt (α := ℝ≥0∞) 1 ∞), HPow.hPow (α := ℝ≥0∞) ∞ z < 1
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : z < 0
top : ∀ (hx : LT.lt (α := ℝ≥0∞) 1 ∞), HPow.hPow (α := ℝ≥0∞) ∞ z < 1
⊢ x ^ z < 1
have coe : ∀ (x : ℝ≥0) (hx : 1 < (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞) ^ z < 1
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx : 1 < (↑x : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞) ^ z < 1
have hx₁ : 1 < x
Tactic: simp only [one_lt_coe_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : z < 0
⊢ x ^ z ≤ 1
have top : ∀ (hx : LE.le (α := ℝ≥0∞) 1 ∞), HPow.hPow (α := ℝ≥0∞) ∞ z ≤ 1
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : z < 0
top : ∀ (hx : LE.le (α := ℝ≥0∞) 1 ∞), HPow.hPow (α := ℝ≥0∞) ∞ z ≤ 1
⊢ x ^ z ≤ 1
have coe : ∀ (x : ℝ≥0) (hx : 1 ≤ (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞) ^ z ≤ 1
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx : 1 ≤ (↑x : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞) ^ z ≤ 1
have hx₁ : 1 ≤ x
Tactic: simp only [one_le_coe_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z
have top : ∀ (hx : LT.lt (α := ℝ≥0∞) 1 ∞), 1 < HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : 0 < z
top : ∀ (hx : LT.lt (α := ℝ≥0∞) 1 ∞), 1 < HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ 1 < x ^ z
have coe : ∀ (x : ℝ≥0) (hx : 1 < (↑x : ℝ≥0∞)), 1 < (↑x : ℝ≥0∞) ^ z
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : 1 < (↑x : ℝ≥0∞)
⊢ 1 < (↑x : ℝ≥0∞) ^ z
have hx₁ : 1 < x
Tactic: simp only [one_lt_coe_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : 0 < z
⊢ 1 ≤ x ^ z
have top : ∀ (hx : LE.le (α := ℝ≥0∞) 1 ∞), 1 ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : 0 < z
top : ∀ (hx : LE.le (α := ℝ≥0∞) 1 ∞), 1 ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ 1 ≤ x ^ z
have coe : ∀ (x : ℝ≥0) (hx : 1 ≤ (↑x : ℝ≥0∞)), 1 ≤ (↑x : ℝ≥0∞) ^ z
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : 1 ≤ (↑x : ℝ≥0∞)
⊢ 1 ≤ (↑x : ℝ≥0∞) ^ z
have hx₁ : 1 ≤ x
Tactic: simp only [one_le_coe_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 < x ^ z
have lift : ∀ (x : ℝ≥0) (hx1 : 0 < (↑x : ℝ≥0∞)) (hx2 : (↑x : ℝ≥0∞) < 1), 1 < (↑x : ℝ≥0∞) ^ z
Tactic: lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx2 le_top)
Cleared hypotheses: x, hx1, hx2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < (↑x : ℝ≥0∞)
hx2 : (↑x : ℝ≥0∞) < 1
⊢ 1 < (↑x : ℝ≥0∞) ^ z
have hx1₁ : 0 < x
Tactic: simp only [coe_lt_one_iff, coe_pos] at hx1 hx2 ⊢
Cleared hypotheses: hx1, hx2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < (↑x : ℝ≥0∞)
hx2 : (↑x : ℝ≥0∞) < 1
hx1₁ : 0 < x
⊢ 1 < (↑x : ℝ≥0∞) ^ z
have hx2₁ : x < 1
Tactic: simp only [coe_lt_one_iff, coe_pos] at hx1 hx2 ⊢
Cleared hypotheses: hx1, hx2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z < 0
⊢ 1 ≤ x ^ z
have lift : ∀ (x : ℝ≥0) (hx1 : 0 < (↑x : ℝ≥0∞)) (hx2 : (↑x : ℝ≥0∞) ≤ 1), 1 ≤ (↑x : ℝ≥0∞) ^ z
Tactic: lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx2 coe_lt_top)
Cleared hypotheses: x, hx1, hx2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < (↑x : ℝ≥0∞)
hx2 : (↑x : ℝ≥0∞) ≤ 1
⊢ 1 ≤ (↑x : ℝ≥0∞) ^ z
have hx1₁ : 0 < x
Tactic: simp only [coe_le_one_iff, coe_pos] at hx1 hx2 ⊢
Cleared hypotheses: hx1, hx2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < (↑x : ℝ≥0∞)
hx2 : (↑x : ℝ≥0∞) ≤ 1
hx1₁ : 0 < x
⊢ 1 ≤ (↑x : ℝ≥0∞) ^ z
have hx2₁ : x ≤ 1
Tactic: simp only [coe_le_one_iff, coe_pos] at hx1 hx2 ⊢
Cleared hypotheses: hx1, hx2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
⊢ (x ^ z).toNNReal = x.toNNReal ^ z
have inl : ∀ (H : z < 0), (x ^ z).toNNReal = x.toNNReal ^ z
Tactic: rcases lt_trichotomy z 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
inl : ∀ (H : z < 0), (x ^ z).toNNReal = x.toNNReal ^ z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z
have inr : ∀ (H : z = 0), (x ^ z).toNNReal = x.toNNReal ^ z
Tactic: rcases lt_trichotomy z 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
inl : ∀ (H : z < 0), (x ^ z).toNNReal = x.toNNReal ^ z
inr : ∀ (H : z = 0), (x ^ z).toNNReal = x.toNNReal ^ z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z
have inr₁ : ∀ (H : 0 < z), (x ^ z).toNNReal = x.toNNReal ^ z
Tactic: rcases lt_trichotomy z 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
H : z < 0
x : ℝ≥0
⊢ ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
have pos : ∀ (hx : x = 0), ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
H : z < 0
x : ℝ≥0
pos : ∀ (hx : x = 0), ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
⊢ ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
have neg : ∀ (hx : ¬x = 0), ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
H : z < 0
⊢ (x ^ z).toNNReal = x.toNNReal ^ z
have inl : (HPow.hPow (α := ℝ≥0∞) ∞ z).toNNReal = ENNReal.toNNReal ∞ ^ z
Tactic: cases x with
    | top => simp [H, ne_of_lt]
    | coe x =>
      by_cases hx : x = 0
      · simp [hx, H, ne_of_lt]
      · simp [← coe_rpow_of_ne_zero hx]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
H : z < 0
inl : (HPow.hPow (α := ℝ≥0∞) ∞ z).toNNReal = ENNReal.toNNReal ∞ ^ z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z
have inl₁ : ∀ (x : ℝ≥0), ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
Tactic: cases x with
    | top => simp [H, ne_of_lt]
    | coe x =>
      by_cases hx : x = 0
      · simp [hx, H, ne_of_lt]
      · simp [← coe_rpow_of_ne_zero hx]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
H : 0 < z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z
have inr : (HPow.hPow (α := ℝ≥0∞) ∞ z).toNNReal = ENNReal.toNNReal ∞ ^ z
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
H : 0 < z
inr : (HPow.hPow (α := ℝ≥0∞) ∞ z).toNNReal = ENNReal.toNNReal ∞ ^ z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z
have inr₁ : ∀ (x : ℝ≥0), ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
⊢ x.toReal ^ z = (x ^ z).toReal
have rw : (↑x.toNNReal : ℝ) ^ z = (x ^ z).toReal
Tactic: rw [ENNReal.toReal, ENNReal.toReal, ← NNReal.coe_rpow, ENNReal.toNNReal_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
rw : (↑x.toNNReal : ℝ) ^ z = (x ^ z).toReal
⊢ x.toReal ^ z = (x ^ z).toReal
have rw₁ : (↑x.toNNReal : ℝ) ^ z = (↑(x ^ z).toNNReal : ℝ)
Tactic: rw [ENNReal.toReal, ENNReal.toReal, ← NNReal.coe_rpow, ENNReal.toNNReal_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
rw : (↑x.toNNReal : ℝ) ^ z = (x ^ z).toReal
rw₁ : (↑x.toNNReal : ℝ) ^ z = (↑(x ^ z).toNNReal : ℝ)
⊢ x.toReal ^ z = (x ^ z).toReal
have rw₂ : (↑(x.toNNReal ^ z) : ℝ) = (↑(x ^ z).toNNReal : ℝ)
Tactic: rw [ENNReal.toReal, ENNReal.toReal, ← NNReal.coe_rpow, ENNReal.toNNReal_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
rw : (↑x.toNNReal : ℝ) ^ z = (x ^ z).toReal
rw₁ : (↑x.toNNReal : ℝ) ^ z = (↑(x ^ z).toNNReal : ℝ)
rw₂ : (↑(x.toNNReal ^ z) : ℝ) = (↑(x ^ z).toNNReal : ℝ)
⊢ x.toReal ^ z = (x ^ z).toReal
have rw₃ : (↑(x.toNNReal ^ z) : ℝ) = (↑(x.toNNReal ^ z) : ℝ)
Tactic: rw [ENNReal.toReal, ENNReal.toReal, ← NNReal.coe_rpow, ENNReal.toNNReal_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x p : ℝ
hx_pos : 0 < x
⊢ (↑x.toNNReal : ℝ≥0∞) ^ p = (↑(x ^ p).toNNReal : ℝ≥0∞)
have h : x.toNNReal ≠ 0
Tactic: rw [← coe_rpow_of_ne_zero, coe_inj, Real.toNNReal_rpow_of_nonneg hx_pos.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
have pos : ∀ (hp0 : p = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
pos : ∀ (hp0 : p = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
have neg : ∀ (hp0 : ¬p = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
have pos : ∀ (hx0 : x = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
pos : ∀ (hx0 : x = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
have neg : ∀ (hx0 : ¬x = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
have hp0₁ : p ≠ 0
Tactic: rw [← Ne] at hp0
Cleared hypotheses: hp0, hx0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
have hp_pos : 0 < p
Tactic: have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg hp0.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
have hx0₁ : x ≠ 0
Tactic: rw [← Ne] at hx0
Cleared hypotheses: hx0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ (x ^ y) ^ y⁻¹ = x
have rw : x ^ (y * y⁻¹) = x
Tactic: rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
rw : x ^ (y * y⁻¹) = x
⊢ (x ^ y) ^ y⁻¹ = x
have rw₁ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
rw : x ^ (y * y⁻¹) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
⊢ (x ^ y) ^ y⁻¹ = x
have rw₂ : x = x
Tactic: rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ (x ^ y⁻¹) ^ y = x
have rw : x ^ (y⁻¹ * y) = x
Tactic: rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
rw : x ^ (y⁻¹ * y) = x
⊢ (x ^ y⁻¹) ^ y = x
have rw₁ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
rw : x ^ (y⁻¹ * y) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
⊢ (x ^ y⁻¹) ^ y = x
have rw₂ : x = x
Tactic: rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑n : ℝ)⁻¹ = x
Tactic: rw [← rpow_natCast, ← rpow_mul, mul_inv_cancel₀ (by positivity), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑n : ℝ)⁻¹ = x
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)⁻¹ = x
Tactic: rw [← rpow_natCast, ← rpow_mul, mul_inv_cancel₀ (by positivity), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑n : ℝ)⁻¹ = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)⁻¹ = x
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have rw₂ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_natCast, ← rpow_mul, mul_inv_cancel₀ (by positivity), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑n : ℝ)⁻¹ = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)⁻¹ = x
rw₂ : HPow.hPow (β := ℝ) x 1 = x
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have rw₃ : x = x
Tactic: rw [← rpow_natCast, ← rpow_mul, mul_inv_cancel₀ (by positivity), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹) (↑n : ℝ) = x
Tactic: rw [← rpow_natCast, ← rpow_mul, inv_mul_cancel₀ (by positivity), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹) (↑n : ℝ) = x
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = x
Tactic: rw [← rpow_natCast, ← rpow_mul, inv_mul_cancel₀ (by positivity), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹) (↑n : ℝ) = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = x
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have rw₂ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_natCast, ← rpow_mul, inv_mul_cancel₀ (by positivity), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹) (↑n : ℝ) = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = x
rw₂ : HPow.hPow (β := ℝ) x 1 = x
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have rw₃ : x = x
Tactic: rw [← rpow_natCast, ← rpow_mul, inv_mul_cancel₀ (by positivity), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
n : ℕ
z : ℝ
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
n : ℕ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw₁ : (x ^ n) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
n : ℕ
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
Tactic: rw [rpow_mul, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
n : ℕ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw₁ : (x ^ y) ^ n = (x ^ y) ^ n
Tactic: rw [rpow_mul, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
n : ℤ
z : ℝ
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
n : ℤ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw₁ : (x ^ n) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
n : ℤ
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
Tactic: rw [rpow_mul, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
n : ℤ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw₁ : (x ^ y) ^ n = (x ^ y) ^ n
Tactic: rw [rpow_mul, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ (a + b) ^ p ≤ (2 * max a b) ^ p
have rw : (a + b) ^ p ≤ (max a b + max a b) ^ p
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ (a + b) ^ p ≤ (max a b + max a b) ^ p
have h₁ : a ≤ max a b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
h₁ : a ≤ max a b
⊢ (a + b) ^ p ≤ (max a b + max a b) ^ p
have h₂ : b ≤ max a b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ HPow.hPow (α := ℝ≥0∞) 2 p * max a b ^ p = HPow.hPow (α := ℝ≥0∞) 2 p * max (a ^ p) (b ^ p)
have rw : HPow.hPow (α := ℝ≥0∞) 2 p * max (a ^ p) (b ^ p) = HPow.hPow (α := ℝ≥0∞) 2 p * max (a ^ p) (b ^ p)
Tactic: rw [max_rpow hp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ HPow.hPow (α := ℝ≥0∞) 2 p * max (a ^ p) (b ^ p) ≤ HPow.hPow (α := ℝ≥0∞) 2 p * (a ^ p + b ^ p)
have bc : max (a ^ p) (b ^ p) ≤ a ^ p + b ^ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ max (a ^ p) (b ^ p) ≤ a ^ p + b ^ p
have bc : 0 ≤ a ^ p
Tactic: apply max_le_add_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
bc : 0 ≤ a ^ p
⊢ max (a ^ p) (b ^ p) ≤ a ^ p + b ^ p
have bc₁ : 0 ≤ b ^ p
Tactic: apply max_le_add_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
b : ℝ
n : ℕ
h : IsNat b n
a : ℝ≥0
⊢ a ^ b = a ^ n
have rw : HPow.hPow (β := ℝ) a (↑n : ℝ) = a ^ n
Tactic: rw [h.1, NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
b : ℝ
n : ℕ
h : IsNat b n
a : ℝ≥0
rw : HPow.hPow (β := ℝ) a (↑n : ℝ) = a ^ n
⊢ a ^ b = a ^ n
have rw₁ : a ^ n = a ^ n
Tactic: rw [h.1, NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
⊢ a ^ b = (a ^ n)⁻¹
have rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
Tactic: rw [h.1, NNReal.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
Tactic: rw [h.1, NNReal.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₂ : a ^ (-Int.ofNat n) = (a ^ n)⁻¹
Tactic: rw [h.1, NNReal.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]