awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
⊢ LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) x) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)
have lift : ∀ (x : ℝ≥0) (hxy : (↑x : ℝ≥0∞) < y),
  LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)
Tactic: lift x to ℝ≥0 using ne_top_of_lt hxy
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : (↑x : ℝ≥0∞) < y
⊢ LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)
have inl : ∀ (hxy : (↑x : ℝ≥0∞) < ∞), LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) ∞)
Tactic: rcases eq_or_ne y ∞ with (rfl | hy)
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : (↑x : ℝ≥0∞) < y
inl : ∀ (hxy : (↑x : ℝ≥0∞) < ∞), LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) ∞)
⊢ LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)
have inr : ∀ (hy : y ≠ ∞), LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)
Tactic: rcases eq_or_ne y ∞ with (rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : (↑x : ℝ≥0∞) < y
hy : y ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)
have inr : ∀ (y : ℝ≥0) (hxy : (↑x : ℝ≥0∞) < (↑y : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑y : ℝ≥0∞))
Tactic: lift y to ℝ≥0 using hy
Cleared hypotheses: y, hxy, hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : 0 < y
x : ℝ≥0∞
⊢ (x ^ (1 / y)) ^ y = x
have rw : x ^ (1 / y * y) = x
Tactic: rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : 0 < y
x : ℝ≥0∞
rw : x ^ (1 / y * y) = x
⊢ (x ^ (1 / y)) ^ y = x
have rw₁ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : 0 < y
x : ℝ≥0∞
rw : x ^ (1 / y * y) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
⊢ (x ^ (1 / y)) ^ y = x
have rw₂ : x = x
Tactic: rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : 0 < y
⊢ (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯
have simp : (StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0∞) ↦ x ^ y) sorry (fun (x : ℝ≥0∞) ↦ x ^ (1 / y)) sorry).symm =
  StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0∞) ↦ x ^ (1 / y)) sorry (fun (x : ℝ≥0∞) ↦ x ^ y) sorry
Tactic: simp only [orderIsoRpow, one_div_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inl : ∀ (hxy : x ≤ y), max x y ^ p = max (x ^ p) (y ^ p)
Tactic: rcases le_total x y with hxy | hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
inl : ∀ (hxy : x ≤ y), max x y ^ p = max (x ^ p) (y ^ p)
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inr : ∀ (hxy : y ≤ x), max x y ^ p = max (x ^ p) (y ^ p)
Tactic: rcases le_total x y with hxy | hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
hxy : x ≤ y
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inl : y ^ p = max (x ^ p) (y ^ p)
Tactic: rw [max_eq_right hxy, max_eq_right (rpow_le_rpow hxy hp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
hxy : x ≤ y
inl : y ^ p = max (x ^ p) (y ^ p)
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inl₁ : y ^ p = y ^ p
Tactic: rw [max_eq_right hxy, max_eq_right (rpow_le_rpow hxy hp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
hxy : y ≤ x
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inr : x ^ p = max (x ^ p) (y ^ p)
Tactic: rw [max_eq_left hxy, max_eq_left (rpow_le_rpow hxy hp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
hxy : y ≤ x
inr : x ^ p = max (x ^ p) (y ^ p)
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inr₁ : x ^ p = x ^ p
Tactic: rw [max_eq_left hxy, max_eq_left (rpow_le_rpow hxy hp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
have nth_rw : HPow.hPow (β := ℝ) x 1 ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
Tactic: nth_rw 1 [← rpow_one x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ HPow.hPow (β := ℝ) x 1 ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
have nth_rw : x ^ (z * z⁻¹) ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
Tactic: nth_rw 1 [← @mul_inv_cancel₀ _ _ z hz.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
have rw : (x ^ z) ^ z⁻¹ ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
Tactic: rw [rpow_mul, @rpow_le_rpow_iff _ _ z⁻¹ (by simp [hz])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
rw : (x ^ z) ^ z⁻¹ ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
⊢ x ^ (z * z⁻¹) ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
have rw₁ : x ^ z ≤ y ↔ x ^ z ≤ y
Tactic: rw [rpow_mul, @rpow_le_rpow_iff _ _ z⁻¹ (by simp [hz])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x < y ^ z⁻¹ ↔ x ^ z < y
have nth_rw : HPow.hPow (β := ℝ) x 1 < y ^ z⁻¹ ↔ x ^ z < y
Tactic: nth_rw 1 [← rpow_one x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ HPow.hPow (β := ℝ) x 1 < y ^ z⁻¹ ↔ x ^ z < y
have nth_rw : x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y
Tactic: nth_rw 1 [← @mul_inv_cancel₀ _ _ z (ne_of_lt hz).symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y
have rw : (x ^ z) ^ z⁻¹ < y ^ z⁻¹ ↔ x ^ z < y
Tactic: rw [rpow_mul, @rpow_lt_rpow_iff _ _ z⁻¹ (by simp [hz])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
rw : (x ^ z) ^ z⁻¹ < y ^ z⁻¹ ↔ x ^ z < y
⊢ x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y
have rw₁ : x ^ z < y ↔ x ^ z < y
Tactic: rw [rpow_mul, @rpow_lt_rpow_iff _ _ z⁻¹ (by simp [hz])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
have nth_rw : x ^ z⁻¹ ≤ HPow.hPow (β := ℝ) y 1 ↔ x ≤ y ^ z
Tactic: nth_rw 1 [← ENNReal.rpow_one y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ HPow.hPow (β := ℝ) y 1 ↔ x ≤ y ^ z
have nth_rw : x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
Tactic: nth_rw 1 [← @mul_inv_cancel₀ _ _ z hz.ne.symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
have rw : x ^ z⁻¹ ≤ (y ^ z) ^ z⁻¹ ↔ x ≤ y ^ z
Tactic: rw [ENNReal.rpow_mul, ENNReal.rpow_le_rpow_iff (inv_pos.2 hz)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
rw : x ^ z⁻¹ ≤ (y ^ z) ^ z⁻¹ ↔ x ≤ y ^ z
⊢ x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
have rw₁ : x ≤ y ^ z ↔ x ≤ y ^ z
Tactic: rw [ENNReal.rpow_mul, ENNReal.rpow_le_rpow_iff (inv_pos.2 hz)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y z : ℝ
hx : 1 < x
hx' : x ≠ ∞
hyz : y < z
⊢ x ^ y < x ^ z
have lift : ∀ (x : ℝ≥0) (hx : 1 < (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞) ^ y < (↑x : ℝ≥0∞) ^ z
Tactic: lift x to ℝ≥0 using hx'
Cleared hypotheses: x, hx, hx'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < (↑x : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞) ^ y < (↑x : ℝ≥0∞) ^ z
have hx₁ : 1 < x
Tactic: rw [one_lt_coe_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z
have top : ∀ (hx : LE.le (α := ℝ≥0∞) 1 ∞), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ 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∞
y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
top : ∀ (hx : LE.le (α := ℝ≥0∞) 1 ∞), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ x ^ y ≤ x ^ z
have coe : ∀ (x : ℝ≥0) (hx : 1 ≤ (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top : ∀ (Hy : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
top : ∀ (Hy : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top₁ : ∀ (Hy : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
top : ∀ (Hy : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : ∀ (Hy : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top₂ : ∀ (Hy : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y < 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y < 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
Hz : z < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top : False
Tactic: simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
Hz : z < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top : False
Tactic: simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
Hz : z = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
have top : False
Tactic: simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
Hz : z < 0
⊢ False
have linarith : y - z + -(y - 0) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
Hz : z < 0
⊢ False
have linarith : y - z + (0 - y) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
Hz : z = 0
⊢ False
have linarith : y - z + (0 - y) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
y z : ℝ
hyz : y ≤ z
x : ℝ≥0
hx : 1 ≤ (↑x : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑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∞
y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z
have lift : ∀ (x : ℝ≥0) (hx0 : 0 < (↑x : ℝ≥0∞)) (hx1 : (↑x : ℝ≥0∞) < 1), (↑x : ℝ≥0∞) ^ y < (↑x : ℝ≥0∞) ^ z
Tactic: lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx1 le_top)
Cleared hypotheses: x, hx0, hx1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < (↑x : ℝ≥0∞)
hx1 : (↑x : ℝ≥0∞) < 1
⊢ (↑x : ℝ≥0∞) ^ y < (↑x : ℝ≥0∞) ^ z
have hx0₁ : 0 < x
Tactic: simp only [coe_lt_one_iff, coe_pos] at hx0 hx1
Cleared hypotheses: hx0, hx1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < (↑x : ℝ≥0∞)
hx1 : (↑x : ℝ≥0∞) < 1
hx0₁ : 0 < x
⊢ (↑x : ℝ≥0∞) ^ y < (↑x : ℝ≥0∞) ^ z
have hx1₁ : x < 1
Tactic: simp only [coe_lt_one_iff, coe_pos] at hx0 hx1
Cleared hypotheses: hx0, hx1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y z : ℝ
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z
have lift : ∀ (x : ℝ≥0) (hx1 : (↑x : ℝ≥0∞) ≤ 1), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx1 coe_lt_top)
Cleared hypotheses: x, hx1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos : ∀ (Hy : y < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
pos : ∀ (Hy : y < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos₁ : ∀ (Hy : y = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
pos : ∀ (Hy : y < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
pos₁ : ∀ (Hy : y = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos₂ : ∀ (Hy : 0 < y), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos₁ : ∀ (Hz : z = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
pos₁ : ∀ (Hz : z = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos₂ : ∀ (Hz : 0 < z), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y = 0
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y = 0
pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos₁ : ∀ (Hz : z = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y = 0
pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
pos₁ : ∀ (Hz : z = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos₂ : ∀ (Hz : 0 < z), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : 0 < y
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : 0 < y
pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos₁ : ∀ (Hz : z = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : 0 < y
pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
pos₁ : ∀ (Hz : z = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos₂ : ∀ (Hz : 0 < z), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos : False
Tactic: simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos : False
Tactic: simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have pos : False
Tactic: simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ False
have linarith : z - y + (y - 0) + -(z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ False
have linarith : z - y + (y - 0) + (0 - z) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ False
have linarith : z - y + (y - 0) + (0 - z) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : ¬x = 0
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
have hx1₁ : x ≤ 1
Tactic: rw [coe_le_one_iff] at hx1
Cleared hypotheses: hx1, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x
have nth_rw : x ^ z ≤ HPow.hPow (β := ℝ) x 1
Tactic: nth_rw 2 [← ENNReal.rpow_one x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ≤ x ^ z
have nth_rw : HPow.hPow (β := ℝ) x 1 ≤ x ^ z
Tactic: nth_rw 1 [← ENNReal.rpow_one x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
⊢ 0 < x ^ p
have pos : ∀ (hp_zero : p = 0), 0 < x ^ p
Tactic: by_cases hp_zero : p = 0