awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (∞ * y) ^ z =
    if (Eq (α := ℝ≥0∞) ∞ 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) ∞ z * y ^ z
have 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
Tactic: rcases hz with hz | hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
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
have 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
Tactic: induction y
Cleared hypotheses: y, hy0, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ ((↑x : ℝ≥0∞) * y) ^ z =
    if ((↑x : ℝ≥0∞) = 0 ∧ y = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ y = 0) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * y ^ z
have 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
Tactic: induction y
Cleared hypotheses: y, hy0, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : (↑x : ℝ≥0∞) ≠ 0
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
have hx0₁ : ¬x = 0
Tactic: rw [ne_eq, coe_eq_zero] at hx0
Cleared hypotheses: hx0, hy0, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
x : ℝ≥0
hx0 : ¬x = 0
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
have 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
Tactic: rcases hz with hz | hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ ((↑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
have 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
Tactic: rcases hz with hz | hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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∞)
⊢ ((↑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
have 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
Tactic: simp only [*]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
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∞) * (↑x_1 : ℝ≥0∞)) ^ z =
    if (False ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ False) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z
have hx0₁ : ¬x = 0
Tactic: norm_cast at *
Cleared hypotheses: hz, hx0, hy0, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
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 : ℝ≥0∞) * (↑x_1 : ℝ≥0∞)) ^ z =
    if (False ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ False) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z
have hy0₁ : ¬x_1 = 0
Tactic: norm_cast at *
Cleared hypotheses: hz, hx0, hy0, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
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 : ℝ≥0∞) * (↑x_1 : ℝ≥0∞)) ^ z =
    if (False ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ False) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z
have hxy₁ : x ≤ x_1
Tactic: norm_cast at *
Cleared hypotheses: hz, hx0, hy0, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
x x_1 : ℝ≥0
hz : z < 0 ∨ 0 < z
hx0 : ¬x = 0
hy0 : ¬x_1 = 0
hxy : x ≤ x_1
⊢ (↑(x * x_1) : ℝ≥0∞) ^ z =
    if (False ∧ (↑x_1 : ℝ≥0∞) = ∞ ∨ (↑x : ℝ≥0∞) = ∞ ∧ False) ∧ z < 0 then ∞ else (↑x : ℝ≥0∞) ^ z * (↑x_1 : ℝ≥0∞) ^ z
have 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
Tactic: rw [← coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), NNReal.mul_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
x x_1 : ℝ≥0
hz : z < 0 ∨ 0 < z
hx0 : ¬x = 0
hy0 : ¬x_1 = 0
hxy : x ≤ x_1
⊢ (↑(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
have 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∞)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ ∏ i ∈ insert a s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ insert a s, f i) : ℝ≥0∞) ^ r
have insert : (↑(f a) : ℝ≥0∞) ^ r * ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(f a * ∏ i ∈ s, f i) : ℝ≥0∞) ^ r
Tactic: simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ ∏ i ∈ Insert.insert a s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ Insert.insert a s, f i) : ℝ≥0∞) ^ r
have insert₁ : (↑(f a) : ℝ≥0∞) ^ r * (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r = (↑(f a * ∏ i ∈ s, f i) : ℝ≥0∞) ^ r
Tactic: simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ ∏ i ∈ Insert.insert a s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ Insert.insert a s, f i) : ℝ≥0∞) ^ r
have insert₂ : ((↑(f a) : ℝ≥0∞) * (↑(∏ i ∈ s, f i) : ℝ≥0∞)) ^ r = (↑(f a * ∏ i ∈ s, f i) : ℝ≥0∞) ^ r
Tactic: simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r
have empty : ∏ i ∈ ∅, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ ∅, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
empty : ∏ i ∈ ∅, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ ∅, f i) : ℝ≥0∞) ^ r
⊢ ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r
have insert : ∀ (a : ι) (s : Finset ι) (hi : a ∉ s) (ih : ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r),
  ∏ i ∈ insert a s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ insert a 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r
have empty : ∏ i ∈ ∅, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ ∅, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
empty : ∏ i ∈ ∅, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ ∅, f i) : ℝ≥0∞) ^ r
⊢ ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r
have insert : ∀ (a : ι) (s : Finset ι) (hi : a ∉ s) (ih : ∏ i ∈ s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ s, f i) : ℝ≥0∞) ^ r),
  ∏ i ∈ insert a s, (↑(f i) : ℝ≥0∞) ^ r = (↑(∏ i ∈ insert a 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, f i ≠ ∞), ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞
⊢ ∏ i ∈ insert i s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ insert i s, f i) r
have h2f : ∀ i ∈ s, f i ≠ ∞
Tactic: have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, f i ≠ ∞), ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞
h2f : ∀ i ∈ s, f i ≠ ∞
⊢ ∏ i ∈ insert i s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ insert i s, f i) r
have insert : Ne (α := ℝ≥0∞) (∏ i ∈ s, f i) ∞
Tactic: rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ∞
r : ℝ
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ ∞),
  ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ∞
r : ℝ
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ ∞),
    ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (ih : ∀ (hf : ∀ i ∈ s, f i ≠ ∞), ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r)
  (hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞), ∏ i ∈ insert i s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ insert i s, f i) r
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ∞
r : ℝ
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ ∞),
  ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ∞
r : ℝ
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ ∞),
    ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (ih : ∀ (hf : ∀ i ∈ s, f i ≠ ∞), ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r)
  (hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞), ∏ i ∈ insert i s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ insert i s, f i) r
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
a : ι
s : Finset ι
hi : a ∉ s
ih : ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
⊢ ∏ i ∈ insert a s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ insert a s, f i) r
have insert : f a ^ r * ∏ i ∈ s, f i ^ r = (f a * ∏ i ∈ s, f i) ^ r
Tactic: simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
a : ι
s : Finset ι
hi : a ∉ s
ih : ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
insert : f a ^ r * ∏ i ∈ s, f i ^ r = (f a * ∏ i ∈ s, f i) ^ r
⊢ ∏ i ∈ Insert.insert a s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ Insert.insert a s, f i) r
have insert₁ : f a ^ r * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r = (f a * ∏ i ∈ s, f i) ^ r
Tactic: simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
have empty : ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
empty : ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
have insert : ∀ (a : ι) (s : Finset ι) (hi : a ∉ s) (ih : ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r),
  ∏ i ∈ insert a s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ insert a s, f i) r
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
have empty : ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
empty : ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
have insert : ∀ (a : ι) (s : Finset ι) (hi : a ∉ s) (ih : ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r),
  ∏ i ∈ insert a s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ insert a s, f i) r
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have inl : HPow.hPow (β := ℝ) x⁻¹ 0 = (HPow.hPow (β := ℝ) x 0)⁻¹
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
inl : HPow.hPow (β := ℝ) x⁻¹ 0 = (HPow.hPow (β := ℝ) x 0)⁻¹
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have inr : ∀ (hy : y ≠ 0), x⁻¹ ^ y = (x ^ y)⁻¹
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have hy₁ : y < 0 ∨ 0 < y
Tactic: replace hy := hy.lt_or_gt
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have inr : HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
Tactic: rcases eq_or_ne x 0 with (rfl | h0)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
inr : HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have inr₁ : ∀ (h0 : x ≠ 0), x⁻¹ ^ y = (x ^ y)⁻¹
Tactic: rcases eq_or_ne x 0 with (rfl | h0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
have inr : y < 0 → HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
Tactic: cases hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y < 0 ∨ 0 < y
inr : y < 0 → HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
have inr₁ : 0 < y → HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
Tactic: cases hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have inr : ∀ (h0 : Ne (α := ℝ≥0∞) ∞ 0), HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
Tactic: rcases eq_or_ne x ⊤ with (rfl | h_top)
Cleared hypotheses: x, h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
inr : ∀ (h0 : Ne (α := ℝ≥0∞) ∞ 0), HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have inr₁ : ∀ (h_top : x ≠ ∞), x⁻¹ ^ y = (x ^ y)⁻¹
Tactic: rcases eq_or_ne x ⊤ with (rfl | h_top)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : Ne (α := ℝ≥0∞) ∞ 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
have inr : y < 0 → HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
Tactic: cases hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : Ne (α := ℝ≥0∞) ∞ 0
inr : y < 0 → HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
have inr₁ : 0 < y → HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
Tactic: cases hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have inr : x⁻¹ ^ y * x ^ y = 1
Tactic: apply ENNReal.eq_inv_of_mul_eq_one_left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ x⁻¹ ^ y * x ^ y = 1
have inr : (x⁻¹ * x) ^ y = 1
Tactic: rw [← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0, ENNReal.inv_mul_cancel h0 h_top,
    one_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
inr : (x⁻¹ * x) ^ y = 1
⊢ x⁻¹ ^ y * x ^ y = 1
have inr₁ : HPow.hPow (α := ℝ≥0∞) 1 y = 1
Tactic: rw [← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0, ENNReal.inv_mul_cancel h0 h_top,
    one_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
inr : (x⁻¹ * x) ^ y = 1
inr₁ : HPow.hPow (α := ℝ≥0∞) 1 y = 1
⊢ x⁻¹ ^ y * x ^ y = 1
have inr₂ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0, ENNReal.inv_mul_cancel h0 h_top,
    one_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ (x / y) ^ z = x ^ z / y ^ z
have rw : (x * y⁻¹) ^ z = x ^ z / y ^ z
Tactic: rw [div_eq_mul_inv, mul_rpow_of_nonneg _ _ hz, inv_rpow, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
rw : (x * y⁻¹) ^ z = x ^ z / y ^ z
⊢ (x / y) ^ z = x ^ z / y ^ z
have rw₁ : x ^ z * y⁻¹ ^ z = x ^ z / y ^ z
Tactic: rw [div_eq_mul_inv, mul_rpow_of_nonneg _ _ hz, inv_rpow, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
rw : (x * y⁻¹) ^ z = x ^ z / y ^ z
rw₁ : x ^ z * y⁻¹ ^ z = x ^ z / y ^ z
⊢ (x / y) ^ z = x ^ z / y ^ z
have rw₂ : x ^ z * (y ^ z)⁻¹ = x ^ z / y ^ z
Tactic: rw [div_eq_mul_inv, mul_rpow_of_nonneg _ _ hz, inv_rpow, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
rw : (x * y⁻¹) ^ z = x ^ z / y ^ z
rw₁ : x ^ z * y⁻¹ ^ z = x ^ z / y ^ z
rw₂ : x ^ z * (y ^ z)⁻¹ = x ^ z / y ^ z
⊢ (x / y) ^ z = x ^ z / y ^ z
have rw₃ : x ^ z * (y ^ z)⁻¹ = x ^ z * (y ^ z)⁻¹
Tactic: rw [div_eq_mul_inv, mul_rpow_of_nonneg _ _ hz, inv_rpow, div_eq_mul_inv]