awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
top₁ : ∀ (H : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
have top₂ : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
have pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
have neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
have pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
have pos₁ : ∀ (H : y = 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
pos₁ : ∀ (H : y = 0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
⊢ (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
have pos₂ : ∀ (H : 0 < y), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ∞ ∧ y < 0
have top : HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
Tactic: cases x with
  | top =>
    rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
    · simp [← coe_rpow_of_ne_zero h, h]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
top : HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
⊢ x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ∞ ∧ y < 0
have coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) ^ y = 0 ↔ (↑x : ℝ≥0∞) = 0 ∧ 0 < y ∨ (↑x : ℝ≥0∞) = ∞ ∧ y < 0
Tactic: cases x with
  | top =>
    rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
    · simp [← coe_rpow_of_ne_zero h, h]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
have top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
have top₁ : ∀ (H : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
top₁ : ∀ (H : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
have top₂ : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
have pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
have neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
have pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
have pos₁ : ∀ (H : y = 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
pos₁ : ∀ (H : y = 0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
⊢ (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
have pos₂ : ∀ (H : 0 < y), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
⊢ x ^ y = ∞ ↔ x = 0 ∧ y < 0 ∨ x = ∞ ∧ 0 < y
have top : HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
Tactic: cases x with
  | top =>
    rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
    · simp [← coe_rpow_of_ne_zero h, h]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
top : HPow.hPow (α := ℝ≥0∞) ∞ y = ∞ ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ y < 0 ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ 0 < y
⊢ x ^ y = ∞ ↔ x = 0 ∧ y < 0 ∨ x = ∞ ∧ 0 < y
have coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) ^ y = ∞ ↔ (↑x : ℝ≥0∞) = 0 ∧ y < 0 ∨ (↑x : ℝ≥0∞) = ∞ ∧ 0 < y
Tactic: cases x with
  | top =>
    rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
    · simp [← coe_rpow_of_ne_zero h, h]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
y z : ℝ
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
h'x : (↑x : ℝ≥0∞) ≠ ∞
⊢ (↑x : ℝ≥0∞) ^ (y + z) = (↑x : ℝ≥0∞) ^ y * (↑x : ℝ≥0∞) ^ z
have this : x ≠ 0
Tactic: have : x ≠ 0 := fun h => by simp [h] at hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
⊢ x ^ (y + z) = x ^ y * x ^ z
have top : ∀ (hx : Ne (α := ℝ≥0∞) ∞ 0) (h'x : Ne (α := ℝ≥0∞) ∞ ∞),
  HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ 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]
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ x ^ (y + z) = x ^ y * x ^ z
have coe : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) ≠ 0) (h'x : (↑x : ℝ≥0∞) ≠ ∞), (↑x : ℝ≥0∞) ^ (y + z) = (↑x : ℝ≥0∞) ^ y * (↑x : ℝ≥0∞) ^ 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]
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z
have top : HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: induction x using recTopCoe
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ x ^ (y + z) = x ^ y * x ^ z
have coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) ^ (y + z) = (↑x : ℝ≥0∞) ^ y * (↑x : ℝ≥0∞) ^ z
Tactic: induction x using recTopCoe
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
have top : ∀ (hy : LE.le (α := ℝ) 0 0),
  HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0 * HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases hy.eq_or_lt with rfl | hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
have top₁ : ∀ (hy : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases hy.eq_or_lt with rfl | hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
hz : 0 ≤ z
hy : LE.le (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0 * HPow.hPow (α := ℝ≥0∞) ∞ z
have top : HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = 1 * HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rw [rpow_zero, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
hz : 0 ≤ z
hy : LE.le (α := ℝ) 0 0
top : HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = 1 * HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0 * HPow.hPow (α := ℝ≥0∞) ∞ z
have top₁ : HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rw [rpow_zero, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (0 + z) = HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0 * HPow.hPow (α := ℝ≥0∞) ∞ z
have top₂ : HPow.hPow (α := ℝ≥0∞) ∞ z = HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rw [rpow_zero, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hy_1 : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
have top : ∀ (hz : LE.le (α := ℝ) 0 0),
  HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0
Tactic: rcases hz.eq_or_lt with rfl | hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
have top₁ : ∀ (hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ (y + z) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) ∞ z
Tactic: rcases hz.eq_or_lt with rfl | hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy_1 : 0 ≤ y
hy : 0 < y
hz : LE.le (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0
have top : HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y * 1
Tactic: rw [rpow_zero, mul_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0
have top₁ : HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y
Tactic: rw [rpow_zero, mul_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y + 0) = HPow.hPow (α := ℝ≥0∞) ∞ y * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0
have top₂ : HPow.hPow (α := ℝ≥0∞) ∞ y = HPow.hPow (α := ℝ≥0∞) ∞ y
Tactic: rw [rpow_zero, mul_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
y z : ℝ
hyz : 0 < y + z
⊢ x ^ (y + z) = x ^ y * x ^ z
have inl : ∀ (hx : Ne (α := ℝ≥0∞) 0 ∞), HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z
Tactic: obtain (rfl | hx') := eq_or_ne x 0
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ x ^ (y + z) = x ^ y * x ^ z
have inr : ∀ (hx' : x ≠ 0), x ^ (y + z) = x ^ y * x ^ z
Tactic: obtain (rfl | hx') := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : 0 < y + z
hx : Ne (α := ℝ≥0∞) 0 ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z
have pos : ∀ (hy' : 0 < y), HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z
Tactic: by_cases hy' : 0 < y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z
have neg : ∀ (hy' : ¬0 < y), HPow.hPow (α := ℝ≥0∞) 0 (y + z) = HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 z
Tactic: by_cases hy' : 0 < y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
hyz : 0 < y + z
hx : Ne (α := ℝ≥0∞) 0 ∞
hy' : ¬0 < y
⊢ 0 < z
have linarith : z ≤ 0 → 0 - (y + z) + (y - 0) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
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
have hz' : 0 < z
Tactic: have hz' : 0 < z := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
y z : ℝ
hyz : 0 < y + z
hx' : x ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z
have inr : x ^ y * x ^ z = x ^ y * x ^ z
Tactic: rw [ENNReal.rpow_add _ _ hx' hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
have top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
have top₁ : ∀ (H : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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)⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
have top₂ : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
⊢ (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
have pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
pos : ∀ (h : x = 0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
⊢ (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
have neg : ∀ (h : ¬x = 0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
⊢ (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
have pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
x : ℝ≥0
h : x = 0
pos : ∀ (H : y < 0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
⊢ (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
have pos₁ : ∀ (H : y = 0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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)⁻¹
⊢ (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
have pos₂ : ∀ (H : 0 < y), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ y)⁻¹
have A : x ^ y ≠ 0
Tactic: have A : x ^ y ≠ 0 := by simp [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹
have top : HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ 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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y : ℝ
top : HPow.hPow (α := ℝ≥0∞) ∞ (-y) = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
⊢ x ^ (-y) = (x ^ y)⁻¹
have coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) ^ (-y) = ((↑x : ℝ≥0∞) ^ 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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
⊢ x ^ (y - z) = x ^ y / x ^ z
have rw : x ^ (y + -z) = x ^ y / x ^ z
Tactic: rw [sub_eq_add_neg, rpow_add _ _ hx h'x, rpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
rw : x ^ (y + -z) = x ^ y / x ^ z
⊢ x ^ (y - z) = x ^ y / x ^ z
have rw₁ : x ^ y * x ^ (-z) = x ^ y / x ^ z
Tactic: rw [sub_eq_add_neg, rpow_add _ _ hx h'x, rpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ x ^ (y - z) = x ^ y / x ^ z
have rw₂ : x ^ y * (x ^ z)⁻¹ = x ^ y / x ^ z
Tactic: rw [sub_eq_add_neg, rpow_add _ _ hx h'x, rpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ x ^ (y - z) = x ^ y / x ^ z
have rw₃ : x ^ y * (x ^ z)⁻¹ = x ^ y * (x ^ z)⁻¹
Tactic: rw [sub_eq_add_neg, rpow_add _ _ hx h'x, rpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top : ∀ (Hy : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥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 : ℝ
top : ∀ (Hy : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top₁ : ∀ (Hy : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥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 : ℝ
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥0∞) ∞ y ^ z
have top₂ : ∀ (Hy : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ (y * z) = HPow.hPow (α := ℝ≥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 : ℝ
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)