awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
top :
  ∀ (hx : Ne (α := ℝ≥0∞) ∞ 0) (h'x : Ne (α := ℝ≥0∞) ∞ ∞),
    HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
coe :
  ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) ≠ 0) (h'x : (↑x : ℝ≥0∞) ≠ ∞), (↑x : ℝ≥0∞) ^ (y + z) = (↑x : ℝ≥0∞) ^ y * (↑x : ℝ≥0∞) ^ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
cases x with
  | top => exact (h'x rfl).elim
  | coe x =>
    have : x ≠ 0 := fun h => by simp [h] at hx
    simp [← coe_rpow_of_ne_zero this, NNReal.rpow_add this]

Premises used: False.elim
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
top : HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) ^ (y + z) = (↑x : ℝ≥0∞) ^ y * (↑x : ℝ≥0∞) ^ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
induction x using recTopCoe
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
top :
  ∀ (hy : LE.le (α := ℝ) 0 0),
    HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0 * HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : ∀ (hy : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
rcases hy.eq_or_lt with rfl | hy

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : 0 ≤ z
hy : LE.le (α := ℝ) 0 0
top : HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = 1 * HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = HPow.hPow (α := ℝ≥0∞) ∞ z
top₂ top₃ : HPow.hPow (α := ℝ≥0∞) ∞ z = HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0 * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
rw [rpow_zero, one_mul, zero_add]

Premises used: zero_add, ENNReal.rpow_zero, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hy_1 : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
top :
  ∀ (hz : LE.le (α := ℝ) 0 0),
    HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0
top₁ : ∀ (hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
rcases hz.eq_or_lt with rfl | hz

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy_1 : 0 ≤ y
hy : 0 < y
hz : LE.le (α := ℝ) 0 0
top : HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y * 1
top₁ : HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y
top₂ top₃ : HPow.hPow (α := ℝ≥0∞) ∞ y = HPow.hPow (α := ℝ≥0∞) ∞ y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0

Tactic:
rw [rpow_zero, mul_one, add_zero]

Premises used: ENNReal.rpow_zero, mul_one, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hy_1 : 0 ≤ y
hz_1 : 0 ≤ z
hy : 0 < y
hz : 0 < z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [top_rpow_of_pos, hy, hz, add_pos hy hz]

Premises used: add_pos, ENNReal.top_rpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
x : ℝ≥0
⊢ (↑x : ℝ≥0∞) ^ (y + z) = (↑x : ℝ≥0∞) ^ y * (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_nonneg, hy, hz, add_nonneg hy hz, NNReal.rpow_add_of_nonneg _ hy hz]

Premises used: ENNReal.coe_rpow_of_nonneg, add_nonneg, NNReal.rpow_add_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
y z : ℝ
hyz : 0 < y + z
inl :
  ∀ (hx : Ne (α := ℝ≥0∞) 0 ∞), HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z
inr : ∀ (hx' : x ≠ 0), x ^ (y + z) = x ^ y * x ^ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
obtain (rfl | hx') := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : 0 < y + z
hx : Ne (α := ℝ≥0∞) 0 ∞
pos : ∀ (hy' : 0 < y), HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z
neg : ∀ (hy' : ¬0 < y), HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z
⊢ HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z

Tactic:
by_cases hy' : 0 < y
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : 0 < y + z
hx : Ne (α := ℝ≥0∞) 0 ∞
hy' : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z

Tactic:
simp [ENNReal.zero_rpow_of_pos hyz, ENNReal.zero_rpow_of_pos hy']

Premises used: ENNReal.zero_rpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : 0 < y + z
hx : Ne (α := ℝ≥0∞) 0 ∞
hy' : ¬0 < y
linarith : z ≤ 0 → 0 - (y + z) + (y - 0) + (z - 0) = 0
⊢ 0 < z

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : 0 < y + z
hx : Ne (α := ℝ≥0∞) 0 ∞
hy' : ¬0 < y
⊢ 0 < z

Tactic:
have hz' : 0 < z := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : 0 < y + z
hx : Ne (α := ℝ≥0∞) 0 ∞
hy' : ¬0 < y
hz' : 0 < z
⊢ HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z

Tactic:
simp [ENNReal.zero_rpow_of_pos hyz, ENNReal.zero_rpow_of_pos hz']

Premises used: ENNReal.zero_rpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
y z : ℝ
hyz : 0 < y + z
hx' : x ≠ 0
inr inr₁ : x ^ y * x ^ z = x ^ y * x ^ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rw [ENNReal.rpow_add _ _ hx' hx]

Premises used: ENNReal.rpow_add
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
top₁ : ∀ (H : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
top₂ : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥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) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹

Tactic:
simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]

Premises used: Iff.mpr, neg_pos, 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) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹

Tactic:
simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]

Premises used: Iff.mpr, neg_pos, 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) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹

Tactic:
simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]

Premises used: Iff.mpr, neg_pos, 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∞) ^ y)⁻¹
neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
⊢ (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥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∞) ^ y)⁻¹
pos₁ : ∀ (H : y = 0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
pos₂ : ∀ (H : 0 < y), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
⊢ (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥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∞) ^ y)⁻¹

Tactic:
simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]

Premises used: Iff.mpr, ENNReal.zero_rpow_of_pos, neg_pos, 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∞) ^ y)⁻¹

Tactic:
simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]

Premises used: Iff.mpr, ENNReal.zero_rpow_of_pos, neg_pos, 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∞) ^ y)⁻¹

Tactic:
simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]

Premises used: Iff.mpr, ENNReal.zero_rpow_of_pos, neg_pos, ENNReal.zero_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0

Tactic:
have A : x ^ y ≠ 0 := by simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
x : ℝ≥0
h : ¬x = 0
A : x ^ y ≠ 0
⊢ (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹

Tactic:
simp [← coe_rpow_of_ne_zero h, ← coe_inv A, NNReal.rpow_neg]

Premises used: ENNReal.coe_inv, ENNReal.coe_rpow_of_ne_zero, NNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
top : HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
cases x with
  | top =>
    rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]
    · have A : x ^ y ≠ 0 := by simp [h]
      simp [← coe_rpow_of_ne_zero h, ← coe_inv A, NNReal.rpow_neg]

Premises used: Iff.mpr, ENNReal.zero_rpow_of_pos, neg_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, NNReal.rpow_neg, OfNat.ofNat, ENNReal.top_rpow_of_neg, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
rw : x ^ (y + -z) = x ^ y / x ^ z
rw₁ : x ^ y * x ^ (-z) = x ^ y / x ^ z
rw₂ : x ^ y * (x ^ z)⁻¹ = x ^ y / x ^ z
rw₃ rw₄ : x ^ y * (x ^ z)⁻¹ = x ^ y * (x ^ z)⁻¹
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
rw [sub_eq_add_neg, rpow_add _ _ hx h'x, rpow_neg, div_eq_mul_inv]

Premises used: ENNReal.rpow_add, sub_eq_add_neg, div_eq_mul_inv, ENNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
⊢ HPow.hPow (β := ℝ) x (-1) = x⁻¹

Tactic:
simp [rpow_neg]

Premises used: ENNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
top : ∀ (Hy : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
top₁ : ∀ (Hy : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
top₂ : ∀ (Hy : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ 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 : ℝ
Hy : y < 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ 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 : ℝ
Hy : y = 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ 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 : ℝ
Hy : 0 < y
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ 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 : ℝ
Hy : y < 0
Hz : z < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z

Tactic:
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
Hy : y < 0
Hz : z = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z

Tactic:
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
Hy : y < 0
Hz : 0 < z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z

Tactic:
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
Hy : y = 0
Hz : z < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z

Tactic:
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
Hy : y = 0
Hz : z = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z

Tactic:
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
Hy : y = 0
Hz : 0 < z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z

Tactic:
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
Hy : 0 < y
Hz : z < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z

Tactic:
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
Hy : 0 < y
Hz : z = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z

Tactic:
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
Hy : 0 < y
Hz : 0 < z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z

Tactic:
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

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

Tactic:
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
          mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

Tactic:
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
          mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

Tactic:
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
          mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

Tactic:
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
          mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

Tactic:
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
          mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

Tactic:
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
          mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

Tactic:
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
          mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

Tactic:
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
          mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

Tactic:
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
          mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, ENNReal.top_rpow_of_pos, ENNReal.zero_rpow_of_neg, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0

Tactic:
have : x ^ y ≠ 0 := by simp [h]