awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
Hz : z < 0
linarith : y - z + -(y - 0) + (z - 0) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
Hz : z < 0
linarith : y - z + (0 - y) + (z - 0) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
Hz : z = 0
linarith : y - z + (0 - y) + (z - 0) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
x : ℝ≥0
hx : 1 ≤ (↑x : ℝ≥0∞)
⊢ 1 ≤ x

Tactic:
simp only [one_le_coe_iff] at hx

Premises used: ENNReal.one_le_coe_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
x : ℝ≥0
hx : 1 ≤ x
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
      NNReal.rpow_le_rpow_of_exponent_le hx hyz]

Premises used: ne_of_gt, ENNReal.coe_rpow_of_ne_zero, zero_lt_one, NNReal.rpow_le_rpow_of_exponent_le, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ≠ ∞

Tactic:
ne_of_lt (lt_of_lt_of_le hx1 le_top)

Premises used: le_top, ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
lift : ∀ (x : ℝ≥0) (hx0 : 0 < (↑x : ℝ≥0∞)) (hx1 : (↑x : ℝ≥0∞) < 1), (↑x : ℝ≥0∞) ^ y < (↑x : ℝ≥0∞) ^ z
⊢ x ^ y < x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx1 le_top)

Premises used: le_top, ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < (↑x : ℝ≥0∞)
hx1 : (↑x : ℝ≥0∞) < 1
⊢ 0 < x

Tactic:
simp only [coe_lt_one_iff, coe_pos] at hx0 hx1

Premises used: ENNReal.coe_pos, ENNReal.coe_lt_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < (↑x : ℝ≥0∞)
hx1 : (↑x : ℝ≥0∞) < 1
hx0₁ : 0 < x
⊢ x < 1

Tactic:
simp only [coe_lt_one_iff, coe_pos] at hx0 hx1

Premises used: ENNReal.coe_pos, ENNReal.coe_lt_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < x
hx1 : x < 1
⊢ (↑x : ℝ≥0∞) ^ y < (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt hx0), NNReal.rpow_lt_rpow_of_exponent_gt hx0 hx1 hyz]

Premises used: NNReal.rpow_lt_rpow_of_exponent_gt, ne_of_gt, ENNReal.coe_rpow_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ≠ ∞

Tactic:
ne_of_lt (lt_of_le_of_lt hx1 coe_lt_top)

Premises used: lt_of_le_of_lt, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hx1 : x ≤ 1
hyz : z ≤ y
lift : ∀ (x : ℝ≥0) (hx1 : (↑x : ℝ≥0∞) ≤ 1), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ x ^ y ≤ x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx1 coe_lt_top)

Premises used: lt_of_le_of_lt, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
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
pos₂ : ∀ (Hy : 0 < y), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
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
pos₂ : ∀ (Hz : 0 < z), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
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
pos₂ : ∀ (Hz : 0 < z), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
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
pos₂ : ∀ (Hz : 0 < z), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
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

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
pos : False
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
pos : False
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
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

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
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

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
pos : False
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
linarith : z - y + (y - 0) + -(z - 0) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
linarith : z - y + (y - 0) + (0 - z) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
linarith : z - y + (y - 0) + (0 - z) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : ¬x = 0
⊢ x ≤ 1

Tactic:
rw [coe_le_one_iff] at hx1

Premises used: ENNReal.coe_le_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : (↑x : ℝ≥0∞) ≤ 1
h : ¬x = 0
hx1₁ : x ≤ 1
⊢ ¬x = 0

Tactic:
rw [coe_le_one_iff] at hx1

Premises used: ENNReal.coe_le_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : x ≤ 1
h : ¬x = 0
⊢ (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero h,
      NNReal.rpow_le_rpow_of_exponent_ge (bot_lt_iff_ne_bot.mpr h) hx1 hyz]

Premises used: Iff.mpr, NNReal.rpow_le_rpow_of_exponent_ge, bot_lt_iff_ne_bot, ENNReal.coe_rpow_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
nth_rw : x ^ z ≤ HPow.hPow (β := ℝ) x 1
⊢ x ^ z ≤ x

Tactic:
nth_rw 2 [← ENNReal.rpow_one x]

Premises used: ENNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ HPow.hPow (β := ℝ) x 1

Tactic:
ENNReal.rpow_le_rpow_of_exponent_ge hx h_one_le

Premises used: ENNReal.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ HPow.hPow (β := ℝ) x 1

Tactic:
exact ENNReal.rpow_le_rpow_of_exponent_ge hx h_one_le

Premises used: ENNReal.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
nth_rw : HPow.hPow (β := ℝ) x 1 ≤ x ^ z
⊢ x ≤ x ^ z

Tactic:
nth_rw 1 [← ENNReal.rpow_one x]

Premises used: ENNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ HPow.hPow (β := ℝ) x 1 ≤ x ^ z

Tactic:
ENNReal.rpow_le_rpow_of_exponent_le hx h_one_le

Premises used: ENNReal.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ HPow.hPow (β := ℝ) x 1 ≤ x ^ z

Tactic:
exact ENNReal.rpow_le_rpow_of_exponent_le hx h_one_le

Premises used: ENNReal.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
pos : ∀ (hp_zero : p = 0), 0 < x ^ p
neg : ∀ (hp_zero : ¬p = 0), 0 < x ^ p
⊢ 0 < x ^ p

Tactic:
by_cases hp_zero : p = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p = 0
⊢ 0 < x ^ p

Tactic:
simp [hp_zero, zero_lt_one]

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ p ≠ 0

Tactic:
rw [← Ne] at hp_zero

Premises used: Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < p

Tactic:
have hp_pos := lt_of_le_of_ne hp_nonneg hp_zero.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
neg : HPow.hPow (α := ℝ≥0∞) 0 p < x ^ p
⊢ 0 < x ^ p

Tactic:
rw [← zero_rpow_of_pos hp_pos]

Premises used: ENNReal.zero_rpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ HPow.hPow (α := ℝ≥0∞) 0 p < x ^ p

Tactic:
rpow_lt_rpow hx_pos hp_pos

Premises used: ENNReal.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ HPow.hPow (α := ℝ≥0∞) 0 p < x ^ p

Tactic:
exact rpow_lt_rpow hx_pos hp_pos

Premises used: ENNReal.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
inl : ∀ (hp_pos : 0 < p), 0 < x ^ p
inr : ∀ (hp_nonpos : p ≤ 0), 0 < x ^ p
⊢ 0 < x ^ p

Tactic:
rcases lt_or_ge 0 p with hp_pos | hp_nonpos

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
rpow_pos_of_nonneg hx_pos (le_of_lt hp_pos)

Premises used: le_of_lt, ENNReal.rpow_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
exact rpow_pos_of_nonneg hx_pos (le_of_lt hp_pos)

Premises used: le_of_lt, ENNReal.rpow_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
inr : x ^ (-p) ≠ ∞
⊢ 0 < x ^ p

Tactic:
rw [← neg_neg p, rpow_neg, ENNReal.inv_pos]

Premises used: neg_neg, ENNReal.rpow_neg, ENNReal.inv_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ x ^ (-p) ≠ ∞

Tactic:
rpow_ne_top_of_nonneg (Right.nonneg_neg_iff.mpr hp_nonpos) hx_ne_top

Premises used: Iff.mpr, Right.nonneg_neg_iff, ENNReal.rpow_ne_top_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ x ^ (-p) ≠ ∞

Tactic:
exact rpow_ne_top_of_nonneg (Right.nonneg_neg_iff.mpr hp_nonpos) hx_ne_top

Premises used: Iff.mpr, Right.nonneg_neg_iff, ENNReal.rpow_ne_top_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : x < 1
hz : 0 < z
⊢ x ≠ ∞

Tactic:
ne_of_lt (lt_of_lt_of_le hx le_top)

Premises used: le_top, ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : x < 1
hz : 0 < z
lift : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) < 1), (↑x : ℝ≥0∞) ^ z < 1
⊢ x ^ z < 1

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx le_top)

Premises used: le_top, ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : (↑x : ℝ≥0∞) < 1
⊢ x < 1

Tactic:
simp only [coe_lt_one_iff] at hx

Premises used: ENNReal.coe_lt_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : x < 1
⊢ (↑x : ℝ≥0∞) ^ z < 1

Tactic:
simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.rpow_lt_one hx hz]

Premises used: NNReal.rpow_lt_one, le_of_lt, ENNReal.coe_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
hz : 0 ≤ z
⊢ x ≠ ∞

Tactic:
ne_of_lt (lt_of_le_of_lt hx coe_lt_top)

Premises used: lt_of_le_of_lt, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
hz : 0 ≤ z
lift : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) ≤ 1), (↑x : ℝ≥0∞) ^ z ≤ 1
⊢ x ^ z ≤ 1

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx coe_lt_top)

Premises used: lt_of_le_of_lt, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≤ 1
⊢ x ≤ 1

Tactic:
simp only [coe_le_one_iff] at hx

Premises used: ENNReal.coe_le_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : x ≤ 1
⊢ (↑x : ℝ≥0∞) ^ z ≤ 1

Tactic:
simp [← coe_rpow_of_nonneg _ hz, NNReal.rpow_le_one hx hz]

Premises used: ENNReal.coe_rpow_of_nonneg, NNReal.rpow_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : z < 0
top : ∀ (hx : LT.lt (α := ℝ≥0∞) 1 ∞), HPow.hPow (α := ℝ≥0∞) ∞ z < 1
coe : ∀ (x : ℝ≥0) (hx : 1 < (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞) ^ z < 1
⊢ x ^ z < 1

Tactic:
cases x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
hx : LT.lt (α := ℝ≥0∞) 1 ∞
⊢ HPow.hPow (α := ℝ≥0∞) ∞ z < 1

Tactic:
simp [top_rpow_of_neg hz, zero_lt_one]

Premises used: zero_lt_one, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx : 1 < (↑x : ℝ≥0∞)
⊢ 1 < x

Tactic:
simp only [one_lt_coe_iff] at hx

Premises used: ENNReal.one_lt_coe_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx : 1 < x
⊢ (↑x : ℝ≥0∞) ^ z < 1

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)),
      NNReal.rpow_lt_one_of_one_lt_of_neg hx hz]

Premises used: lt_trans, ne_of_gt, ENNReal.coe_rpow_of_ne_zero, zero_lt_one, NNReal.rpow_lt_one_of_one_lt_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : z < 0
top : ∀ (hx : LE.le (α := ℝ≥0∞) 1 ∞), HPow.hPow (α := ℝ≥0∞) ∞ z ≤ 1
coe : ∀ (x : ℝ≥0) (hx : 1 ≤ (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞) ^ z ≤ 1
⊢ x ^ z ≤ 1

Tactic:
cases x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
hx : LE.le (α := ℝ≥0∞) 1 ∞
⊢ HPow.hPow (α := ℝ≥0∞) ∞ z ≤ 1

Tactic:
simp [top_rpow_of_neg hz]

Premises used: ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx : 1 ≤ (↑x : ℝ≥0∞)
⊢ 1 ≤ x

Tactic:
simp only [one_le_coe_iff] at hx

Premises used: ENNReal.one_le_coe_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx : 1 ≤ x
⊢ (↑x : ℝ≥0∞) ^ z ≤ 1

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
      NNReal.rpow_le_one_of_one_le_of_nonpos hx (le_of_lt hz)]

Premises used: NNReal.rpow_le_one_of_one_le_of_nonpos, le_of_lt, ne_of_gt, ENNReal.coe_rpow_of_ne_zero, zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : 0 < z
top : ∀ (hx : LT.lt (α := ℝ≥0∞) 1 ∞), 1 < HPow.hPow (α := ℝ≥0∞) ∞ z
coe : ∀ (x : ℝ≥0) (hx : 1 < (↑x : ℝ≥0∞)), 1 < (↑x : ℝ≥0∞) ^ z
⊢ 1 < x ^ z

Tactic:
cases x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 < z
hx : LT.lt (α := ℝ≥0∞) 1 ∞
⊢ 1 < HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [top_rpow_of_pos hz]

Premises used: ENNReal.top_rpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : 1 < (↑x : ℝ≥0∞)
⊢ 1 < x

Tactic:
simp only [one_lt_coe_iff] at hx

Premises used: ENNReal.one_lt_coe_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : 1 < x
⊢ 1 < (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_lt_rpow hx hz]

Premises used: le_of_lt, ENNReal.coe_rpow_of_nonneg, NNReal.one_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : 0 < z
top : ∀ (hx : LE.le (α := ℝ≥0∞) 1 ∞), 1 ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
coe : ∀ (x : ℝ≥0) (hx : 1 ≤ (↑x : ℝ≥0∞)), 1 ≤ (↑x : ℝ≥0∞) ^ z
⊢ 1 ≤ x ^ z

Tactic:
cases x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 < z
hx : LE.le (α := ℝ≥0∞) 1 ∞
⊢ 1 ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [top_rpow_of_pos hz]

Premises used: ENNReal.top_rpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : 1 ≤ (↑x : ℝ≥0∞)
⊢ 1 ≤ x

Tactic:
simp only [one_le_coe_iff] at hx

Premises used: ENNReal.one_le_coe_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : 1 ≤ x
⊢ 1 ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_le_rpow hx (le_of_lt hz)]

Premises used: NNReal.one_le_rpow, le_of_lt, ENNReal.coe_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ x ≠ ∞

Tactic:
ne_of_lt (lt_of_lt_of_le hx2 le_top)

Premises used: le_top, ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
lift : ∀ (x : ℝ≥0) (hx1 : 0 < (↑x : ℝ≥0∞)) (hx2 : (↑x : ℝ≥0∞) < 1), 1 < (↑x : ℝ≥0∞) ^ z
⊢ 1 < x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx2 le_top)

Premises used: le_top, ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < (↑x : ℝ≥0∞)
hx2 : (↑x : ℝ≥0∞) < 1
⊢ 0 < x

Tactic:
simp only [coe_lt_one_iff, coe_pos] at hx1 hx2 ⊢

Premises used: ENNReal.coe_pos, ENNReal.coe_lt_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < (↑x : ℝ≥0∞)
hx2 : (↑x : ℝ≥0∞) < 1
hx1₁ : 0 < x
⊢ x < 1

Tactic:
simp only [coe_lt_one_iff, coe_pos] at hx1 hx2 ⊢

Premises used: ENNReal.coe_pos, ENNReal.coe_lt_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x < 1
⊢ 1 < (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt hx1), NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg hx1 hx2 hz]

Premises used: ne_of_gt, NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg, ENNReal.coe_rpow_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z < 0
⊢ x ≠ ∞

Tactic:
ne_of_lt (lt_of_le_of_lt hx2 coe_lt_top)

Premises used: lt_of_le_of_lt, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z < 0
lift : ∀ (x : ℝ≥0) (hx1 : 0 < (↑x : ℝ≥0∞)) (hx2 : (↑x : ℝ≥0∞) ≤ 1), 1 ≤ (↑x : ℝ≥0∞) ^ z
⊢ 1 ≤ x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx2 coe_lt_top)

Premises used: lt_of_le_of_lt, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < (↑x : ℝ≥0∞)
hx2 : (↑x : ℝ≥0∞) ≤ 1
⊢ 0 < x

Tactic:
simp only [coe_le_one_iff, coe_pos] at hx1 hx2 ⊢

Premises used: ENNReal.coe_le_one_iff, ENNReal.coe_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < (↑x : ℝ≥0∞)
hx2 : (↑x : ℝ≥0∞) ≤ 1
hx1₁ : 0 < x
⊢ x ≤ 1

Tactic:
simp only [coe_le_one_iff, coe_pos] at hx1 hx2 ⊢

Premises used: ENNReal.coe_le_one_iff, ENNReal.coe_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x ≤ 1
⊢ 1 ≤ (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt hx1),
    NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos hx1 hx2 (le_of_lt hz)]

Premises used: le_of_lt, ne_of_gt, ENNReal.coe_rpow_of_ne_zero, NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
inl : ∀ (H : z < 0), (x ^ z).toNNReal = x.toNNReal ^ z
inr : ∀ (H : z = 0), (x ^ z).toNNReal = x.toNNReal ^ z
inr₁ : ∀ (H : 0 < z), (x ^ z).toNNReal = x.toNNReal ^ z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Tactic:
rcases lt_trichotomy z 0 with (H | H | H)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
H : z < 0
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ z).toNNReal = ENNReal.toNNReal ∞ ^ z

Tactic:
simp [H, ne_of_lt]

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
H : z < 0
x : ℝ≥0
pos : ∀ (hx : x = 0), ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
neg : ∀ (hx : ¬x = 0), ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
⊢ ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
H : z < 0
x : ℝ≥0
hx : x = 0
⊢ ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z

Tactic:
simp [hx, H, ne_of_lt]

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
H : z < 0
x : ℝ≥0
hx : ¬x = 0
⊢ ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z

Tactic:
simp [← coe_rpow_of_ne_zero hx]

Premises used: ENNReal.coe_rpow_of_ne_zero