awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
rw : HPow.hPow (β := ℝ) (↑x : ℝ) (↑n : ℝ)⁻¹ ^ n = (↑x : ℝ)
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x

Tactic:
rw [← NNReal.coe_inj, NNReal.coe_pow, coe_rpow]

Premises used: NNReal.coe_rpow, NNReal.coe_pow, NNReal.coe_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (β := ℝ) (↑x : ℝ) (↑n : ℝ)⁻¹ ^ n = (↑x : ℝ)

Tactic:
Real.rpow_inv_natCast_pow x.2 hn

Premises used: Real.rpow_inv_natCast_pow, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (β := ℝ) (↑x : ℝ) (↑n : ℝ)⁻¹ ^ n = (↑x : ℝ)

Tactic:
exact Real.rpow_inv_natCast_pow x.2 hn

Premises used: Real.rpow_inv_natCast_pow, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ
hx : 0 ≤ x
nth_rw : ((↑x.toNNReal : ℝ) ^ y).toNNReal = x.toNNReal ^ y
⊢ (x ^ y).toNNReal = x.toNNReal ^ y

Tactic:
nth_rw 1 [← Real.coe_toNNReal x hx]

Premises used: Real.coe_toNNReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ
hx : 0 ≤ x
rw : (↑(x.toNNReal ^ y) : ℝ).toNNReal = x.toNNReal ^ y
rw₁ rw₂ : x.toNNReal ^ y = x.toNNReal ^ y
⊢ ((↑x.toNNReal : ℝ) ^ y).toNNReal = x.toNNReal ^ y

Tactic:
rw [← NNReal.coe_rpow, Real.toNNReal_coe]

Premises used: NNReal.coe_rpow, Real.toNNReal_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
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)

Tactic:
simp only [NNReal.rpow_lt_rpow hxy h]

Premises used: NNReal.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h : 0 ≤ z
h0 : 0 = z
⊢ Monotone (β := ℝ≥0) fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x 0

Tactic:
simp only [rpow_zero, monotone_const]

Premises used: monotone_const, NNReal.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x_1 : ℝ≥0
w y_1 z y : ℝ
hy : 0 < y
x : ℝ≥0
rw : x ^ (1 / y * y) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
rw₂ rw₃ : x = x
⊢ (x ^ (1 / y)) ^ y = x

Tactic:
rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]

Premises used: NNReal.rpow_mul, Ne.symm, one_div_mul_cancel, NNReal.rpow_one, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : 0 < y
simp :
  (StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0) ↦ x ^ y) ⋯ (fun (x : ℝ≥0) ↦ x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0) ↦ x ^ (1 / y)) ⋯ (fun (x : ℝ≥0) ↦ x ^ y) ⋯
⊢ (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯

Tactic:
simp only [orderIsoRpow, one_div_one_div]

Premises used: NNReal.orderIsoRpow, one_div_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : 0 < y
⊢ (StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0) ↦ x ^ y) ⋯ (fun (x : ℝ≥0) ↦ x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0) ↦ x ^ (1 / y)) ⋯ (fun (x : ℝ≥0) ↦ x ^ y) ⋯

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ
hx : 0 ≤ x
a : (↑‖x ^ y‖₊ : ℝ) = (↑(‖x‖₊ ^ y) : ℝ)
⊢ ‖x ^ y‖₊ = ‖x‖₊ ^ y

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ (↑‖x ^ y‖₊ : ℝ) = (↑(‖x‖₊ ^ y) : ℝ)

Tactic:
Real.norm_rpow_of_nonneg hx

Premises used: Real.norm_rpow_of_nonneg, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ (↑‖x ^ y‖₊ : ℝ) = (↑(‖x‖₊ ^ y) : ℝ)

Tactic:
exact Real.norm_rpow_of_nonneg hx

Premises used: Real.norm_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
⊢ x.rpow y = x ^ y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0 = 1
coe : ∀ (x : ℝ≥0), HPow.hPow (β := ℝ) (↑x : ℝ≥0∞) 0 = 1
⊢ HPow.hPow (β := ℝ) x 0 = 1

Tactic:
cases x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
⊢ Eq (α := ℝ≥0∞)
    (match (motive := ℝ≥0∞ → ℝ → ℝ≥0∞) ∞, 0 with
      | some x, y => if x = 0 ∧ y < 0 then ∞ else (↑(x.rpow y) : ℝ≥0∞)
      | none, y => if 0 < y then ∞ else if y = 0 then 1 else 0 :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
simp [← none_eq_top]

Premises used: ENNReal.none_eq_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ (if x = 0 ∧ LT.lt (α := ℝ) 0 0 then ∞ else (↑(x.rpow 0) : ℝ≥0∞)) = 1

Tactic:
simp [← none_eq_top]

Premises used: ENNReal.none_eq_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
rw : LT.lt (α := ℝ≥0∞) 0 1
⊢ 0 < HPow.hPow (β := ℝ) x 0

Tactic:
rw [rpow_zero]

Premises used: ENNReal.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
⊢ LT.lt (α := ℝ≥0∞) 0 1

Tactic:
one_pos

Premises used: one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
⊢ LT.lt (α := ℝ≥0∞) 0 1

Tactic:
exact one_pos

Premises used: one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = if 0 < y then ∞ else if y = 0 then 1 else 0

Tactic:
rfl

Premises used: ENNReal.rpow, rfl, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = ∞

Tactic:
simp [top_rpow_def, h]

Premises used: ENNReal.top_rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : y < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = 0

Tactic:
simp [top_rpow_def, asymm h, ne_of_lt h]

Premises used: asymm, ENNReal.top_rpow_def, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : 0 < y
⊢ (if Eq (α := ℝ≥0) 0 0 ∧ y < 0 then ∞ else (↑(NNReal.rpow 0 y) : ℝ≥0∞)) = some 0

Tactic:
simp [asymm h, ne_of_gt h]

Premises used: asymm, ne_of_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : y < 0
⊢ (if Eq (α := ℝ≥0) 0 0 ∧ y < 0 then ∞ else (↑(NNReal.rpow 0 y) : ℝ≥0∞)) = ∞

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
inl : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞
inr : HPow.hPow (α := ℝ≥0∞) (β := ℝ) 0 0 = if LT.lt (α := ℝ) 0 0 then 0 else if Eq (α := ℝ) 0 0 then 1 else ∞
inr₁ : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
rcases lt_trichotomy (0 : ℝ) y with (H | rfl | H)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
H : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
simp [H, zero_rpow_of_pos]

Premises used: ENNReal.zero_rpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
⊢ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 0 0 = if LT.lt (α := ℝ) 0 0 then 0 else if Eq (α := ℝ) 0 0 then 1 else ∞

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
H : y < 0
⊢ HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
simp [H, asymm H, ne_of_lt, zero_rpow_of_neg]

Premises used: asymm, ENNReal.zero_rpow_of_neg, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
rw :
  HMul.hMul (α := ℝ≥0∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) =
    if 0 < y then 0 else if y = 0 then 1 else ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 y = HPow.hPow (α := ℝ≥0∞) 0 y

Tactic:
rw [zero_rpow_def]

Premises used: ENNReal.zero_rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
pos : 0 < y → HMul.hMul (α := ℝ≥0∞) 0 0 = 0
pos₁ : ¬0 < y → y = 0 → HMul.hMul (α := ℝ≥0∞) 1 1 = 1
neg : ¬0 < y → ¬y = 0 → HMul.hMul (α := ℝ≥0∞) ∞ ∞ = ∞
⊢ HMul.hMul (α := ℝ≥0∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) =
    if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : 0 < y
⊢ HMul.hMul (α := ℝ≥0∞) 0 0 = 0

Tactic:
zero_mul _

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : ¬0 < y
h_1 : y = 0
⊢ HMul.hMul (α := ℝ≥0∞) 1 1 = 1

Tactic:
one_mul _

Premises used: one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : ¬0 < y
h_1 : ¬y = 0
⊢ HMul.hMul (α := ℝ≥0∞) ∞ ∞ = ∞

Tactic:
top_mul_top

Premises used: ENNReal.top_mul_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : 0 < y
⊢ HMul.hMul (α := ℝ≥0∞) 0 0 = 0

Tactic:
exacts [zero_mul _, one_mul _, top_mul_top]

Premises used: MulZeroClass.zero_mul, ENNReal.top_mul_top, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ some (x.rpow y) = if x = 0 ∧ y < 0 then ∞ else (↑(x.rpow y) : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
pos : ∀ (hx : x = 0), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
neg : ∀ (hx : ¬x = 0), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
⊢ (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
pos : ∀ (H : 0 = y), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
pos₁ : ∀ (H : 0 < y), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
⊢ (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y

Tactic:
rcases le_iff_eq_or_lt.1 h with (H | H)

Premises used: le_iff_eq_or_lt, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 = y
⊢ (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y

Tactic:
simp [hx, H.symm]

Premises used: Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 < y
⊢ (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y

Tactic:
simp [hx, zero_rpow_of_pos H, NNReal.zero_rpow (ne_of_gt H)]

Premises used: NNReal.zero_rpow, ENNReal.zero_rpow_of_pos, ne_of_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y

Tactic:
coe_rpow_of_ne_zero hx _

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

Tactic:
exact coe_rpow_of_ne_zero hx _

Premises used: ENNReal.coe_rpow_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ (↑x : ℝ≥0∞) ^ y = if x = 0 ∧ y < 0 then ∞ else (↑(x ^ y) : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.rpow, rfl, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
M : ℝ≥0
P : ℝ
hP : 0 ≤ P
rw : (↑M : ℝ≥0∞) ^ P = (↑M : ℝ≥0∞) ^ P
rw₁ rw₂ : (↑M : ℝ≥0∞).rpow P = (↑M : ℝ≥0∞).rpow P
⊢ (↑M : ℝ≥0∞) ^ P = (↑(M ^ P) : ℝ≥0∞)

Tactic:
rw [ENNReal.coe_rpow_of_nonneg _ hP, ← ENNReal.rpow_eq_pow]

Premises used: ENNReal.coe_rpow_of_nonneg, ENNReal.rpow_eq_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 1 = ∞
coe : ∀ (x : ℝ≥0), HPow.hPow (β := ℝ) (↑x : ℝ≥0∞) 1 = (↑x : ℝ≥0∞)
⊢ HPow.hPow (β := ℝ) x 1 = x

Tactic:
cases x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
⊢ HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 1 = ∞

Tactic:
dif_pos zero_lt_one

Premises used: ENNReal.rpow, dif_pos, dite, zero_lt_one, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
⊢ HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 1 = ∞

Tactic:
exact dif_pos zero_lt_one

Premises used: dif_pos, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
coe : x = 0 → LT.lt (α := ℝ) 1 0 → False
⊢ (if x = 0 ∧ LT.lt (α := ℝ) 1 0 then ∞ else (↑(HPow.hPow (β := ℝ) x 1) : ℝ≥0∞)) = (↑x : ℝ≥0∞)

Tactic:
simp only [NNReal.rpow_one, ite_eq_right_iff, top_ne_coe, and_imp]

Premises used: ENNReal.top_ne_coe, and_imp, ite_eq_right_iff, NNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ x = 0 → LT.lt (α := ℝ) 1 0 → False

Tactic:
fun _ => zero_le_one.not_gt

Premises used: zero_le_one, LE.le.not_gt, Not
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ x = 0 → LT.lt (α := ℝ) 1 0 → False

Tactic:
exact fun _ => zero_le_one.not_gt

Premises used: zero_le_one, LE.le.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ
rw : (↑(HPow.hPow (α := ℝ≥0) 1 x) : ℝ≥0∞) = (↑1 : ℝ≥0∞)
⊢ HPow.hPow (α := ℝ≥0∞) 1 x = 1

Tactic:
rw [← coe_one, ← coe_rpow_of_ne_zero one_ne_zero]

Premises used: ENNReal.coe_one, ENNReal.coe_rpow_of_ne_zero, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ
⊢ (↑(HPow.hPow (α := ℝ≥0) 1 x) : ℝ≥0∞) = (↑1 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
top₁ : ∀ (H : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
top₂ : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0

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

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
H : y < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0

Tactic:
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Premises used: le_of_lt, ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
H : y = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0

Tactic:
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Premises used: le_of_lt, ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
H : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0

Tactic:
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Premises used: le_of_lt, ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
pos₁ : ∀ (H : y = 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
pos₂ : ∀ (H : 0 < y), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0

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

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

Premises used: ENNReal.zero_rpow_of_pos, le_of_lt, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

Premises used: ENNReal.zero_rpow_of_pos, le_of_lt, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

Premises used: ENNReal.zero_rpow_of_pos, le_of_lt, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0

Tactic:
simp [← coe_rpow_of_ne_zero h, h]

Premises used: ENNReal.coe_rpow_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
top : HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
⊢ x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ∞ ∧ y < 0

Tactic:
cases x with
  | top =>
    rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
    · simp [← coe_rpow_of_ne_zero h, h]

Premises used: ENNReal.zero_rpow_of_pos, le_of_lt, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, OfNat.ofNat, ENNReal.top_rpow_of_neg, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy : 0 < y
⊢ x ^ y = 0 ↔ x = 0

Tactic:
simp [hy, hy.not_gt]

Premises used: LT.lt.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
top₁ : ∀ (H : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
top₂ : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y

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

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
H : y < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y

Tactic:
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Premises used: le_of_lt, ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
H : y = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y

Tactic:
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Premises used: le_of_lt, ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
H : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y

Tactic:
simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Premises used: le_of_lt, ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
pos₁ : ∀ (H : y = 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
pos₂ : ∀ (H : 0 < y), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y

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

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

Premises used: ENNReal.zero_rpow_of_pos, le_of_lt, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

Premises used: ENNReal.zero_rpow_of_pos, le_of_lt, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

Premises used: ENNReal.zero_rpow_of_pos, le_of_lt, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y

Tactic:
simp [← coe_rpow_of_ne_zero h, h]

Premises used: ENNReal.coe_rpow_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
top : HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
⊢ x ^ y = ∞ ↔ x = 0 ∧ y < 0 ∨ x = ∞ ∧ 0 < y

Tactic:
cases x with
  | top =>
    rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
    · simp [← coe_rpow_of_ne_zero h, h]

Premises used: ENNReal.zero_rpow_of_pos, le_of_lt, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, OfNat.ofNat, ENNReal.top_rpow_of_neg, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy : 0 < y
⊢ x ^ y = ∞ ↔ x = ∞

Tactic:
simp [rpow_eq_top_iff, hy, asymm hy]

Premises used: asymm, ENNReal.rpow_eq_top_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy : 0 < y
⊢ x ^ y < ∞ ↔ x < ∞

Tactic:
simp only [lt_top_iff_ne_top, Ne, rpow_eq_top_iff_of_pos hy]

Premises used: Ne, lt_top_iff_ne_top, ENNReal.rpow_eq_top_iff_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x ^ y = ∞ → x = ∞

Tactic:
simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt]

Premises used: ENNReal.rpow_eq_top_iff, LE.le.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x ≠ ∞
⊢ x ^ y ≠ ∞

Tactic:
mt (ENNReal.rpow_eq_top_of_nonneg x hy0) h

Premises used: ENNReal.rpow_eq_top_of_nonneg, mt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0∞
hx : 0 < x
hx' : x ≠ ∞
h : x ^ y = ∞
⊢ False

Tactic:
simp [rpow_eq_top_iff, hx.ne', hx'] at h

Premises used: ENNReal.rpow_eq_top_iff, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x ≠ ∞
⊢ x ^ y < ∞

Tactic:
lt_top_iff_ne_top.mpr (ENNReal.rpow_ne_top_of_nonneg hy0 h)

Premises used: Iff.mpr, ENNReal.rpow_ne_top_of_nonneg, lt_top_iff_ne_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hx : x ≠ 0
hx' : x ≠ ∞
⊢ x ^ y ≠ ∞

Tactic:
simp [rpow_eq_top_iff, hx, hx']

Premises used: ENNReal.rpow_eq_top_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hx : Ne (α := ℝ≥0∞) ∞ 0
h'x : Ne (α := ℝ≥0∞) ∞ ∞
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
(h'x rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hx : Ne (α := ℝ≥0∞) ∞ 0
h'x : Ne (α := ℝ≥0∞) ∞ ∞
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
exact (h'x rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
h'x : (↑x : ℝ≥0∞) ≠ ∞
h : x = 0
⊢ False

Tactic:
simp [h] at hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
h'x : (↑x : ℝ≥0∞) ≠ ∞
⊢ x ≠ 0

Tactic:
have : x ≠ 0 := fun h => by simp [h] at hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
h'x : (↑x : ℝ≥0∞) ≠ ∞
this : x ≠ 0
⊢ (↑x : ℝ≥0∞) ^ (y + z) = (↑x : ℝ≥0∞) ^ y * (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero this, NNReal.rpow_add this]

Premises used: ENNReal.coe_rpow_of_ne_zero, NNReal.rpow_add