awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
x : ℝ≥0
h : ¬x = 0
this : x ^ y ≠ 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero, h, this, NNReal.rpow_mul]

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

Tactic:
cases x with
  | top =>
    rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
        rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
      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]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
          rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
        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]
    · have : x ^ y ≠ 0 := by simp [h]
      simp [← coe_rpow_of_ne_zero, h, this, NNReal.rpow_mul]

Premises used: mul_neg_of_neg_of_pos, ENNReal.zero_rpow_of_pos, NNReal.rpow_mul, ENNReal.top_rpow_of_pos, ENNReal.coe_rpow_of_ne_zero, ENNReal.zero_rpow_of_neg, OfNat.ofNat, mul_pos_of_neg_of_neg, ENNReal.top_rpow_of_neg, mul_neg_of_pos_of_neg, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
n : ℕ
top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑n : ℝ) = HPow.hPow (α := ℝ≥0∞) ∞ n
coe : ∀ (x : ℝ≥0), HPow.hPow (β := ℝ) (↑x : ℝ≥0∞) (↑n : ℝ) = (↑x : ℝ≥0∞) ^ n
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n

Tactic:
cases x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
n : ℕ
top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑0 : ℝ) = HPow.hPow (α := ℝ≥0∞) (β := ℕ) ∞ 0
top₁ : ∀ (n : ℕ), HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑(n + 1) : ℝ) = HPow.hPow (α := ℝ≥0∞) ∞ (n + 1)
⊢ HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑n : ℝ) = HPow.hPow (α := ℝ≥0∞) ∞ n

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

Tactic:
simp [top_rpow_of_pos (Nat.cast_add_one_pos _), top_pow (Nat.succ_ne_zero _)]

Premises used: Nat.cast_add_one_pos, ENNReal.top_rpow_of_pos, ENNReal.top_pow, Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
n : ℕ
⊢ HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑(n + 1) : ℝ) = HPow.hPow (α := ℝ≥0∞) ∞ (n + 1)

Tactic:
simp [top_rpow_of_pos (Nat.cast_add_one_pos _), top_pow (Nat.succ_ne_zero _)]

Premises used: Nat.cast_add_one_pos, ENNReal.top_rpow_of_pos, ENNReal.top_pow, Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
n : ℕ
x : ℝ≥0
⊢ HPow.hPow (β := ℝ) (↑x : ℝ≥0∞) (↑n : ℝ) = (↑x : ℝ≥0∞) ^ n

Tactic:
simp [← coe_rpow_of_nonneg _ (Nat.cast_nonneg n)]

Premises used: Nat.cast_nonneg, ENNReal.coe_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
n : ℕ
inst : n.AtLeastTwo
⊢ HPow.hPow (β := ℝ) x (OfNat.ofNat n) = HPow.hPow (β := ℕ) x (OfNat.ofNat n)

Tactic:
rpow_natCast x n

Premises used: ENNReal.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
n : ℤ
ofNat : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.ofNat a) : ℝ) = x ^ Int.ofNat a
negSucc : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.negSucc a) : ℝ) = x ^ Int.negSucc a
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n

Tactic:
cases n
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
a : ℕ
⊢ HPow.hPow (β := ℝ) x (↑(Int.ofNat a) : ℝ) = x ^ Int.ofNat a

Tactic:
simp only [Int.ofNat_eq_natCast, Int.cast_natCast, rpow_natCast, zpow_natCast,
    Int.cast_negSucc, rpow_neg, zpow_negSucc]

Premises used: zpow_natCast, Int.cast_natCast, zpow_negSucc, ENNReal.rpow_natCast, Int.ofNat_eq_natCast, Int.cast_negSucc, ENNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
a : ℕ
⊢ HPow.hPow (β := ℝ) x (↑(Int.negSucc a) : ℝ) = x ^ Int.negSucc a

Tactic:
simp only [Int.ofNat_eq_natCast, Int.cast_natCast, rpow_natCast, zpow_natCast,
    Int.cast_negSucc, rpow_neg, zpow_negSucc]

Premises used: zpow_natCast, Int.cast_natCast, zpow_negSucc, ENNReal.rpow_natCast, Int.ofNat_eq_natCast, Int.cast_negSucc, ENNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
⊢ HPow.hPow (β := ℝ) x 2 = HPow.hPow (β := ℕ) x 2

Tactic:
rpow_ofNat x 2

Premises used: ENNReal.rpow_ofNat, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
inl :
  HPow.hPow (β := ℝ) (x * y) 0 =
    if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ LT.lt (α := ℝ) 0 0 then ∞ else HPow.hPow (β := ℝ) x 0 * HPow.hPow (β := ℝ) y 0
inr : ∀ (hz : z ≠ 0), (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
rcases eq_or_ne z 0 with (rfl | hz)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
⊢ HPow.hPow (β := ℝ) (x * y) 0 =
    if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ LT.lt (α := ℝ) 0 0 then ∞ else HPow.hPow (β := ℝ) x 0 * HPow.hPow (β := ℝ) y 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z ≠ 0
⊢ z < 0 ∨ 0 < z

Tactic:
replace hz := hz.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
inr :
  ∀
    (this :
      ∀ (x y : ℝ≥0∞) (z : ℝ) (hz : z < 0 ∨ 0 < z) (hxy : x ≤ y),
        (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z)
    (hxy : ¬x ≤ y), (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
wlog :
  ∀ (x y : ℝ≥0∞) (z : ℝ) (hz : z < 0 ∨ 0 < z) (hxy : x ≤ y),
    (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
wlog hxy : x ≤ y
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ) (hz : z < 0 ∨ 0 < z) (hxy : x ≤ y),
    (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ (y * x) ^ z = if (y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0 then ∞ else y ^ z * x ^ z

Tactic:
this y x z hz (le_of_not_ge hxy)

Premises used: le_of_not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ) (hz : z < 0 ∨ 0 < z) (hxy : x ≤ y),
    (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
h : x * y = y * x
h₁ : (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 ↔ (y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0
h₂ : ¬((y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0) → x ^ z * y ^ z = y ^ z * x ^ z
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
convert! this y x z hz (le_of_not_ge hxy) using 2

Premises used: le_of_not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ) (hz : z < 0 ∨ 0 < z) (hxy : x ≤ y),
    (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ x * y = y * x

Tactic:
simp only [mul_comm, and_comm, or_comm]

Premises used: and_comm, mul_comm, or_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ) (hz : z < 0 ∨ 0 < z) (hxy : x ≤ y),
    (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 ↔ (y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0

Tactic:
simp only [mul_comm, and_comm, or_comm]

Premises used: and_comm, mul_comm, or_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ) (hz : z < 0 ∨ 0 < z) (hxy : x ≤ y),
    (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
h : ¬((y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0)
⊢ x ^ z * y ^ z = y ^ z * x ^ z

Tactic:
simp only [mul_comm, and_comm, or_comm]

Premises used: and_comm, mul_comm, or_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
inl :
  ∀ (hxy : 0 ≤ y),
    (0 * y) ^ z =
      if (Eq (α := ℝ≥0∞) 0 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) 0 z * y ^ z
inr : ∀ (hx0 : x ≠ 0), (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
rcases eq_or_ne x 0 with (rfl | hx0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ y
inl :
  ∀ (hxy : LE.le (α := ℝ≥0∞) 0 ∞),
    HMul.hMul (α := ℝ≥0∞) 0 ∞ ^ z =
      if (Eq (α := ℝ≥0∞) 0 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
      else HPow.hPow (α := ℝ≥0∞) 0 z * HPow.hPow (α := ℝ≥0∞) ∞ z
inl₁ :
  ∀ (x : ℝ≥0) (hxy : 0 ≤ (↑x : ℝ≥0∞)),
    (0 * (↑x : ℝ≥0∞)) ^ z =
      if (Eq (α := ℝ≥0∞) 0 0 ∧ (↑x : ℝ≥0∞) = ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ (↑x : ℝ≥0∞) = 0) ∧ z < 0 then ∞
      else HPow.hPow (α := ℝ≥0∞) 0 z * (↑x : ℝ≥0∞) ^ z
⊢ (0 * y) ^ z =
    if (Eq (α := ℝ≥0∞) 0 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) 0 z * y ^ z

Tactic:
induction y
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : LE.le (α := ℝ≥0∞) 0 ∞
inl :
  ∀ (hz : z < 0),
    HMul.hMul (α := ℝ≥0∞) 0 ∞ ^ z =
      if (Eq (α := ℝ≥0∞) 0 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
      else HPow.hPow (α := ℝ≥0∞) 0 z * HPow.hPow (α := ℝ≥0∞) ∞ z
inl₁ :
  ∀ (hz : 0 < z),
    HMul.hMul (α := ℝ≥0∞) 0 ∞ ^ z =
      if (Eq (α := ℝ≥0∞) 0 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
      else HPow.hPow (α := ℝ≥0∞) 0 z * HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HMul.hMul (α := ℝ≥0∞) 0 ∞ ^ z =
    if (Eq (α := ℝ≥0∞) 0 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
    else HPow.hPow (α := ℝ≥0∞) 0 z * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
rcases hz with hz | hz
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hxy : 0 ≤ (↑x : ℝ≥0∞)
inl :
  ∀ (hz : z < 0),
    (0 * (↑x : ℝ≥0∞)) ^ z =
      if (Eq (α := ℝ≥0∞) 0 0 ∧ (↑x : ℝ≥0∞) = ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ (↑x : ℝ≥0∞) = 0) ∧ z < 0 then ∞
      else HPow.hPow (α := ℝ≥0∞) 0 z * (↑x : ℝ≥0∞) ^ z
inl₁ :
  ∀ (hz : 0 < z),
    (0 * (↑x : ℝ≥0∞)) ^ z =
      if (Eq (α := ℝ≥0∞) 0 0 ∧ (↑x : ℝ≥0∞) = ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ (↑x : ℝ≥0∞) = 0) ∧ z < 0 then ∞
      else HPow.hPow (α := ℝ≥0∞) 0 z * (↑x : ℝ≥0∞) ^ z
⊢ (0 * (↑x : ℝ≥0∞)) ^ z =
    if (Eq (α := ℝ≥0∞) 0 0 ∧ (↑x : ℝ≥0∞) = ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ (↑x : ℝ≥0∞) = 0) ∧ z < 0 then ∞
    else HPow.hPow (α := ℝ≥0∞) 0 z * (↑x : ℝ≥0∞) ^ z

Tactic:
rcases hz with hz | hz
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hxy : LE.le (α := ℝ≥0∞) 0 ∞
hz : z < 0
⊢ HMul.hMul (α := ℝ≥0∞) 0 ∞ ^ z =
    if (Eq (α := ℝ≥0∞) 0 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
    else HPow.hPow (α := ℝ≥0∞) 0 z * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [*, hz.not_gt]

Premises used: LT.lt.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hxy : LE.le (α := ℝ≥0∞) 0 ∞
hz : 0 < z
⊢ HMul.hMul (α := ℝ≥0∞) 0 ∞ ^ z =
    if (Eq (α := ℝ≥0∞) 0 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
    else HPow.hPow (α := ℝ≥0∞) 0 z * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [*, hz.not_gt]

Premises used: LT.lt.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
x : ℝ≥0
hxy : 0 ≤ (↑x : ℝ≥0∞)
hz : z < 0
⊢ (0 * (↑x : ℝ≥0∞)) ^ z =
    if (Eq (α := ℝ≥0∞) 0 0 ∧ (↑x : ℝ≥0∞) = ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ (↑x : ℝ≥0∞) = 0) ∧ z < 0 then ∞
    else HPow.hPow (α := ℝ≥0∞) 0 z * (↑x : ℝ≥0∞) ^ z

Tactic:
simp [*, hz.not_gt]

Premises used: LT.lt.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
x : ℝ≥0
hxy : 0 ≤ (↑x : ℝ≥0∞)
hz : 0 < z
⊢ (0 * (↑x : ℝ≥0∞)) ^ z =
    if (Eq (α := ℝ≥0∞) 0 0 ∧ (↑x : ℝ≥0∞) = ∞ ∨ Eq (α := ℝ≥0∞) 0 ∞ ∧ (↑x : ℝ≥0∞) = 0) ∧ z < 0 then ∞
    else HPow.hPow (α := ℝ≥0∞) 0 z * (↑x : ℝ≥0∞) ^ z

Tactic:
simp [*, hz.not_gt]

Premises used: LT.lt.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
inr :
  ∀ (hxy : x ≤ 0),
    (x * 0) ^ z =
      if (x = 0 ∧ Eq (α := ℝ≥0∞) 0 ∞ ∨ x = ∞ ∧ Eq (α := ℝ≥0∞) 0 0) ∧ z < 0 then ∞ else x ^ z * HPow.hPow (α := ℝ≥0∞) 0 z
inr₁ : ∀ (hy0 : y ≠ 0), (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
rcases eq_or_ne y 0 with (rfl | hy0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hx0 : x ≠ 0
hxy : x ≤ 0
⊢ (x * 0) ^ z =
    if (x = 0 ∧ Eq (α := ℝ≥0∞) 0 ∞ ∨ x = ∞ ∧ Eq (α := ℝ≥0∞) 0 0) ∧ z < 0 then ∞ else x ^ z * HPow.hPow (α := ℝ≥0∞) 0 z

Tactic:
(hx0 (bot_unique hxy)).elim

Premises used: False.elim, bot_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hx0 : x ≠ 0
hxy : x ≤ 0
⊢ (x * 0) ^ z =
    if (x = 0 ∧ Eq (α := ℝ≥0∞) 0 ∞ ∨ x = ∞ ∧ Eq (α := ℝ≥0∞) 0 0) ∧ z < 0 then ∞ else x ^ z * HPow.hPow (α := ℝ≥0∞) 0 z

Tactic:
exact (hx0 (bot_unique hxy)).elim

Premises used: False.elim, bot_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
hy0 : y ≠ 0
inr :
  ∀ (hxy : ∞ ≤ y) (hx0 : Ne (α := ℝ≥0∞) ∞ 0),
    (∞ * y) ^ z =
      if (Eq (α := ℝ≥0∞) ∞ 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) ∞ z * y ^ z
inr₁ :
  ∀ (x : ℝ≥0) (hxy : (↑x : ℝ≥0∞) ≤ y) (hx0 : (↑x : ℝ≥0∞) ≠ 0),
    ((↑x : ℝ≥0∞) * y) ^ z =
      if ((↑x : ℝ≥0∞) = 0 ∧ y = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ y = 0) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * y ^ z
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
induction x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : Ne (α := ℝ≥0∞) ∞ 0
inr :
  ∀ (hz : z < 0),
    (∞ * y) ^ z =
      if (Eq (α := ℝ≥0∞) ∞ 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) ∞ z * y ^ z
inr₁ :
  ∀ (hz : 0 < z),
    (∞ * y) ^ z =
      if (Eq (α := ℝ≥0∞) ∞ 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) ∞ z * y ^ z
⊢ (∞ * y) ^ z =
    if (Eq (α := ℝ≥0∞) ∞ 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) ∞ z * y ^ z

Tactic:
rcases hz with hz | hz
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : Ne (α := ℝ≥0∞) ∞ 0
hz : z < 0
⊢ (∞ * y) ^ z =
    if (Eq (α := ℝ≥0∞) ∞ 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) ∞ z * y ^ z

Tactic:
simp [hz, top_unique hxy]

Premises used: top_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : Ne (α := ℝ≥0∞) ∞ 0
hz : 0 < z
⊢ (∞ * y) ^ z =
    if (Eq (α := ℝ≥0∞) ∞ 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) ∞ z * y ^ z

Tactic:
simp [hz, top_unique hxy]

Premises used: top_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
x : ℝ≥0
hxy : (↑x : ℝ≥0∞) ≤ y
hx0 : (↑x : ℝ≥0∞) ≠ 0
inr :
  ∀ (hy0 : Ne (α := ℝ≥0∞) ∞ 0) (hxy : (↑x : ℝ≥0∞) ≤ ∞),
    ((↑x : ℝ≥0∞) * ∞) ^ z =
      if ((↑x : ℝ≥0∞) = 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
      else (↑x : ℝ≥0∞) ^ z * HPow.hPow (α := ℝ≥0∞) ∞ z
inr₁ :
  ∀ (x_1 : ℝ≥0) (hy0 : (↑x_1 : ℝ≥0∞) ≠ 0) (hxy : (↑x : ℝ≥0∞) ≤ (↑x_1 : ℝ≥0∞)),
    ((↑x : ℝ≥0∞) * (↑x_1 : ℝ≥0∞)) ^ z =
      if ((↑x : ℝ≥0∞) = 0 ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ (↑x_1 : ℝ≥0∞) = 0) ∧ z < 0 then ∞
      else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z
⊢ ((↑x : ℝ≥0∞) * y) ^ z =
    if ((↑x : ℝ≥0∞) = 0 ∧ y = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ y = 0) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * y ^ z

Tactic:
induction y
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : (↑x : ℝ≥0∞) ≠ 0
hy0 : Ne (α := ℝ≥0∞) ∞ 0
hxy : (↑x : ℝ≥0∞) ≤ ∞
⊢ ¬x = 0

Tactic:
rw [ne_eq, coe_eq_zero] at hx0

Premises used: ENNReal.coe_eq_zero, ne_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : (↑x : ℝ≥0∞) ≠ 0
hy0 : Ne (α := ℝ≥0∞) ∞ 0
hxy : (↑x : ℝ≥0∞) ≤ ∞
hx0₁ : ¬x = 0
⊢ Ne (α := ℝ≥0∞) ∞ 0

Tactic:
rw [ne_eq, coe_eq_zero] at hx0

Premises used: ENNReal.coe_eq_zero, ne_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : (↑x : ℝ≥0∞) ≠ 0
hy0 : Ne (α := ℝ≥0∞) ∞ 0
hxy : (↑x : ℝ≥0∞) ≤ ∞
hx0₁ : ¬x = 0
hy0₁ : Ne (α := ℝ≥0∞) ∞ 0
⊢ (↑x : ℝ≥0∞) ≤ ∞

Tactic:
rw [ne_eq, coe_eq_zero] at hx0

Premises used: ENNReal.coe_eq_zero, ne_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : ¬x = 0
hy0 : Ne (α := ℝ≥0∞) ∞ 0
hxy : (↑x : ℝ≥0∞) ≤ ∞
inr :
  ∀ (hz : z < 0),
    ((↑x : ℝ≥0∞) * ∞) ^ z =
      if ((↑x : ℝ≥0∞) = 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
      else (↑x : ℝ≥0∞) ^ z * HPow.hPow (α := ℝ≥0∞) ∞ z
inr₁ :
  ∀ (hz : 0 < z),
    ((↑x : ℝ≥0∞) * ∞) ^ z =
      if ((↑x : ℝ≥0∞) = 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
      else (↑x : ℝ≥0∞) ^ z * HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ ((↑x : ℝ≥0∞) * ∞) ^ z =
    if ((↑x : ℝ≥0∞) = 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
    else (↑x : ℝ≥0∞) ^ z * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
rcases hz with hz | hz
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
x : ℝ≥0
hx0 : ¬x = 0
hy0 : Ne (α := ℝ≥0∞) ∞ 0
hxy : (↑x : ℝ≥0∞) ≤ ∞
hz : z < 0
⊢ ((↑x : ℝ≥0∞) * ∞) ^ z =
    if ((↑x : ℝ≥0∞) = 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
    else (↑x : ℝ≥0∞) ^ z * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
x : ℝ≥0
hx0 : ¬x = 0
hy0 : Ne (α := ℝ≥0∞) ∞ 0
hxy : (↑x : ℝ≥0∞) ≤ ∞
hz : 0 < z
⊢ ((↑x : ℝ≥0∞) * ∞) ^ z =
    if ((↑x : ℝ≥0∞) = 0 ∧ Eq (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ Eq (α := ℝ≥0∞) ∞ 0) ∧ z < 0 then ∞
    else (↑x : ℝ≥0∞) ^ z * HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : (↑x : ℝ≥0∞) ≠ 0
x_1 : ℝ≥0
hy0 : (↑x_1 : ℝ≥0∞) ≠ 0
hxy : (↑x : ℝ≥0∞) ≤ (↑x_1 : ℝ≥0∞)
inr :
  ((↑x : ℝ≥0∞) * (↑x_1 : ℝ≥0∞)) ^ z =
    if (False ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ False) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z
⊢ ((↑x : ℝ≥0∞) * (↑x_1 : ℝ≥0∞)) ^ z =
    if ((↑x : ℝ≥0∞) = 0 ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ (↑x_1 : ℝ≥0∞) = 0) ∧ z < 0 then ∞
    else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z

Tactic:
simp only [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : (↑x : ℝ≥0∞) ≠ 0
x_1 : ℝ≥0
hy0 : (↑x_1 : ℝ≥0∞) ≠ 0
hxy : (↑x : ℝ≥0∞) ≤ (↑x_1 : ℝ≥0∞)
⊢ z < 0 ∨ 0 < z

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : (↑x : ℝ≥0∞) ≠ 0
x_1 : ℝ≥0
hy0 : (↑x_1 : ℝ≥0∞) ≠ 0
hxy : (↑x : ℝ≥0∞) ≤ (↑x_1 : ℝ≥0∞)
hz₁ : z < 0 ∨ 0 < z
⊢ ¬x = 0

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : (↑x : ℝ≥0∞) ≠ 0
x_1 : ℝ≥0
hy0 : (↑x_1 : ℝ≥0∞) ≠ 0
hxy : (↑x : ℝ≥0∞) ≤ (↑x_1 : ℝ≥0∞)
hz₁ : z < 0 ∨ 0 < z
hx0₁ : ¬x = 0
⊢ ¬x_1 = 0

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : (↑x : ℝ≥0∞) ≠ 0
x_1 : ℝ≥0
hy0 : (↑x_1 : ℝ≥0∞) ≠ 0
hxy : (↑x : ℝ≥0∞) ≤ (↑x_1 : ℝ≥0∞)
hz₁ : z < 0 ∨ 0 < z
hx0₁ : ¬x = 0
hy0₁ : ¬x_1 = 0
⊢ x ≤ x_1

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
x x_1 : ℝ≥0
hz : z < 0 ∨ 0 < z
hx0 : ¬x = 0
hy0 : ¬x_1 = 0
hxy : x ≤ x_1
inr :
  (↑(x ^ z * x_1 ^ z) : ℝ≥0∞) =
    if (False ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ False) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z
⊢ (↑(x * x_1) : ℝ≥0∞) ^ z =
    if (False ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ False) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z

Tactic:
rw [← coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), NNReal.mul_rpow]

Premises used: ENNReal.coe_rpow_of_ne_zero, mul_ne_zero, NNReal.mul_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
x x_1 : ℝ≥0
hz : z < 0 ∨ 0 < z
hx0 : ¬x = 0
hy0 : ¬x_1 = 0
hxy : x ≤ x_1
inr inr₁ inr₂ inr₃ :
  (↑(x ^ z * x_1 ^ z) : ℝ≥0∞) =
    if (False ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ False) ∧ z < 0 then ∞ else (↑(x ^ z * x_1 ^ z) : ℝ≥0∞)
⊢ (↑(x ^ z * x_1 ^ z) : ℝ≥0∞) =
    if (False ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ False) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
hx : x ≠ ∞
hy : y ≠ ∞
z : ℝ
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
simp [*, mul_rpow_eq_ite]

Premises used: ENNReal.mul_rpow_eq_ite
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
⊢ ((↑x : ℝ≥0∞) * (↑y : ℝ≥0∞)) ^ z = (↑x : ℝ≥0∞) ^ z * (↑y : ℝ≥0∞) ^ z

Tactic:
mul_rpow_of_ne_top coe_ne_top coe_ne_top z

Premises used: ENNReal.mul_rpow_of_ne_top, ENNReal.coe_ne_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ ∅, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ ∅, f i) : ℝ≥0∞) ^ r

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
f : ι → ℝ≥0
r : ℝ
a : ι
s : Finset ι
hi : a ∉ s
ih : ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r
insert : (↑(f a) : ℝ≥0∞) ^ r * ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(f a * ∏ i ∈ s, f i) : ℝ≥0∞) ^ r
insert₁ : (↑(f a) : ℝ≥0∞) ^ r * (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r = (↑(f a * ∏ i ∈ s, f i) : ℝ≥0∞) ^ r
insert₂ : ((↑(f a) : ℝ≥0∞) * (↑(∏ i ∈ s, f i) : ℝ≥0∞)) ^ r = (↑(f a * ∏ i ∈ s, f i) : ℝ≥0∞) ^ r
⊢ ∏ i ∈ Insert.insert a s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ Insert.insert a s, f i) : ℝ≥0∞) ^ r

Tactic:
simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]

Premises used: Finset.prod_insert, ENNReal.coe_mul, ENNReal.coe_mul_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
empty : ∏ i ∈ ∅, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ ∅, f i) : ℝ≥0∞) ^ r
insert :
  ∀ (a : ι) (s : Finset ι) (hi : a ∉ s) (ih : ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r),
    ∏ i ∈ Insert.insert a s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ Insert.insert a s, f i) : ℝ≥0∞) ^ r
⊢ ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]

Premises used: Insert.insert, ENNReal.coe_mul, ENNReal.coe_mul_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
empty : ∏ i ∈ ∅, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ ∅, f i) : ℝ≥0∞) ^ r
insert :
  ∀ (a : ι) (s : Finset ι) (hi : a ∉ s) (ih : ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r),
    ∏ i ∈ Insert.insert a s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ Insert.insert a s, f i) : ℝ≥0∞) ^ r
⊢ ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]

Premises used: Insert.insert, ENNReal.coe_mul, ENNReal.coe_mul_rpow