awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
Hy : y < 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
Hy : y = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
Hy : y = 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
Hy : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
Hy : 0 < y
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos : ∀ (Hy : y < 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
pos : ∀ (Hy : y < 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos₁ : ∀ (Hy : y = 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos₂ : ∀ (Hy : 0 < y), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy y 0 with (Hy | Hy | Hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos₁ : ∀ (Hz : z = 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos₂ : ∀ (Hz : 0 < z), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos₁ : ∀ (Hz : z = 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos₂ : ∀ (Hz : 0 < z), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
pos : ∀ (Hz : z < 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos₁ : ∀ (Hz : z = 0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have pos₂ : ∀ (Hz : 0 < z), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
Tactic: rcases lt_trichotomy z 0 with (Hz | Hz | Hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ y) ^ z
have this : x ^ y ≠ 0
Tactic: have : x ^ y ≠ 0 := by simp [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z
have top : HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ 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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y z : ℝ
top : HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z
have coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) ^ (y * z) = ((↑x : ℝ≥0∞) ^ 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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
n : ℕ
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n
have top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑n : ℝ) = HPow.hPow (α := ℝ≥0∞) ∞ n
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
n : ℕ
top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑n : ℝ) = HPow.hPow (α := ℝ≥0∞) ∞ n
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n
have coe : ∀ (x : ℝ≥0), HPow.hPow (β := ℝ) (↑x : ℝ≥0∞) (↑n : ℝ) = (↑x : ℝ≥0∞) ^ n
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑n : ℝ) = HPow.hPow (α := ℝ≥0∞) ∞ n
have top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑0 : ℝ) = HPow.hPow (α := ℝ≥0∞) (β := ℕ) ∞ 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
n : ℕ
top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑0 : ℝ) = HPow.hPow (α := ℝ≥0∞) (β := ℕ) ∞ 0
⊢ HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑n : ℝ) = HPow.hPow (α := ℝ≥0∞) ∞ n
have top₁ : ∀ (n : ℕ), HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ (↑(n + 1) : ℝ) = HPow.hPow (α := ℝ≥0∞) ∞ (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
n : ℤ
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n
have ofNat : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.ofNat a) : ℝ) = x ^ Int.ofNat a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
n : ℤ
ofNat : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.ofNat a) : ℝ) = x ^ Int.ofNat a
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n
have negSucc : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.negSucc a) : ℝ) = x ^ Int.negSucc a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have 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
Tactic: rcases eq_or_ne z 0 with (rfl | hz)
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have inr : ∀ (hz : z ≠ 0), (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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have hz₁ : z < 0 ∨ 0 < z
Tactic: replace hz := hz.lt_or_gt
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have 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
Tactic: wlog hxy : x ≤ y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have 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
Tactic: wlog hxy : x ≤ y
Cleared hypotheses: x, y, z, hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have h : x * y = y * x
Tactic: convert! this y x z hz (le_of_not_ge hxy) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have h₁ : (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 ↔ (y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0
Tactic: convert! this y x z hz (le_of_not_ge hxy) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have h₂ : ¬((y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0) → x ^ z * y ^ z = y ^ z * x ^ z
Tactic: convert! this y x z hz (le_of_not_ge hxy) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
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
have 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
Tactic: rcases eq_or_ne x 0 with (rfl | hx0)
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have inr : ∀ (hx0 : x ≠ 0), (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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
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
have 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
Tactic: induction y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (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
have 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
Tactic: induction y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
hz : z < 0 ∨ 0 < z
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
have 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
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
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
⊢ 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
have 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
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
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
have 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
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
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
⊢ (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
have 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
Tactic: rcases hz with hz | hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have 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
Tactic: rcases eq_or_ne y 0 with (rfl | hy0)
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have inr₁ : ∀ (hy0 : y ≠ 0), (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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have 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
Tactic: induction x
Cleared hypotheses: x, hxy, hx0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
have 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
Tactic: induction x
Cleared hypotheses: x, hxy, hx0
-- 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
⊢ (∞ * y) ^ z =
    if (Eq (α := ℝ≥0∞) ∞ 0 ∧ y = ∞ ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y = 0) ∧ z < 0 then ∞ else HPow.hPow (α := ℝ≥0∞) ∞ z * y ^ z
have 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
Tactic: rcases hz with hz | hz
Cleared hypotheses: hz