awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
have top : 0 ≤ HPow.hPow (β := ℕ∞) z ⊤
Tactic: rw [lt_one_iff_eq_zero.1 x_0, zero_epow_top]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
have top : HPow.hPow (β := ℕ∞) x ⊤ ≤ ⊤
Tactic: rw [epow_top (x_2.trans_le x_z)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
have refine_1 : ∀ (h : x ^ y = 0), x = 0
Tactic: refine ⟨fun h ↦ ⟨?_, fun y_0 ↦ ?_⟩, fun h ↦ h.1.symm ▸ zero_epow h.2⟩
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
refine_1 : ∀ (h : x ^ y = 0), x = 0
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
have refine_2 : ∀ (h : x ^ y = 0) (y_0 : y = 0), False
Tactic: refine ⟨fun h ↦ ⟨?_, fun y_0 ↦ ?_⟩, fun h ↦ h.1.symm ▸ zero_epow h.2⟩
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
h : x ^ y = 0
⊢ x = 0
have refine_1 : ∀ (x_0 : ¬x = 0), False
Tactic: by_contra x_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (hypothesis)
Goal:
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
⊢ False
have h₁ : Eq (α := ℕ∞) 1 0
Tactic: rw [y_0, epow_zero] at h
Cleared hypotheses: h, y_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
h : x = 1 ∨ y = 0
⊢ x ^ y = 1
have inl : ∀ (h : x = 1), x ^ y = 1
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
h : x = 1 ∨ y = 0
inl : ∀ (h : x = 1), x ^ y = 1
⊢ x ^ y = 1
have inr : ∀ (h : y = 0), x ^ y = 1
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
⊢ x ^ y = 1 ↔ x = 1 ∨ y = 0
have refine : ∀ (h : x ^ y = 1) (y_0 : ¬y = 0), x = 1
Tactic: refine ⟨fun h ↦ or_iff_not_imp_right.2 fun y_0 ↦ ?_, fun h ↦ by rcases h with h | h <;> simp [h]⟩
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
⊢ x = 1
have inl : ∀ (x_0 : x < 1), x = 1
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
inl : ∀ (x_0 : x < 1), x = 1
⊢ x = 1
have inr : ∀ (h : HPow.hPow (α := ℕ∞) 1 y = 1), Eq (α := ℕ∞) 1 1
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
inl : ∀ (x_0 : x < 1), x = 1
inr : ∀ (h : HPow.hPow (α := ℕ∞) 1 y = 1), Eq (α := ℕ∞) 1 1
⊢ x = 1
have inr₁ : ∀ (x_2 : 1 < x), x = 1
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (hypothesis)
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1
have h₁ : Eq (α := ℕ∞) 0 1
Tactic: rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0] at h
Cleared hypotheses: h, y_0, x_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (hypothesis)
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1
have this : LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) 1) ((fun (y : ℕ∞) ↦ x ^ y) y)
Tactic: have := epow_right_mono (one_le_iff_ne_zero.1 x_2.le) (one_le_iff_ne_zero.2 y_0)
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (hypothesis)
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
this : LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) 1) ((fun (y : ℕ∞) ↦ x ^ y) y)
⊢ x = 1
have this₁ : x ≤ 1
Tactic: simp only [epow_one, h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
⊢ x ^ (y + z) = x ^ y * x ^ z
have inl : ∀ (x_0 : x < 1), x ^ (y + z) = x ^ y * x ^ z
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
inl : ∀ (x_0 : x < 1), x ^ (y + z) = x ^ y * x ^ z
⊢ x ^ (y + z) = x ^ y * x ^ z
have inr : HPow.hPow (α := ℕ∞) 1 (y + z) = HPow.hPow (α := ℕ∞) 1 y * HPow.hPow (α := ℕ∞) 1 z
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
inl : ∀ (x_0 : x < 1), x ^ (y + z) = x ^ y * x ^ z
inr : HPow.hPow (α := ℕ∞) 1 (y + z) = HPow.hPow (α := ℕ∞) 1 y * HPow.hPow (α := ℕ∞) 1 z
⊢ x ^ (y + z) = x ^ y * x ^ z
have inr₁ : ∀ (x_2 : 1 < x), x ^ (y + z) = x ^ y * x ^ z
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_0 : x < 1
⊢ x ^ (y + z) = x ^ y * x ^ z
have inl : HPow.hPow (α := ℕ∞) 0 (y + z) = HPow.hPow (α := ℕ∞) 0 y * HPow.hPow (α := ℕ∞) 0 z
Tactic: rw [lt_one_iff_eq_zero.1 x_0]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_0 : x < 1
⊢ HPow.hPow (α := ℕ∞) 0 (y + z) = HPow.hPow (α := ℕ∞) 0 y * HPow.hPow (α := ℕ∞) 0 z
have inl : HPow.hPow (α := ℕ∞) 0 (0 + z) = HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 0 * HPow.hPow (α := ℕ∞) 0 z
Tactic: rcases eq_zero_or_pos y with rfl | y_0
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_0 : x < 1
inl : 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 inl₁ : ∀ (y_0 : 0 < y), HPow.hPow (α := ℕ∞) 0 (y + z) = HPow.hPow (α := ℕ∞) 0 y * HPow.hPow (α := ℕ∞) 0 z
Tactic: rcases eq_zero_or_pos y with rfl | y_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ HPow.hPow (α := ℕ∞) 0 (y + z) = HPow.hPow (α := ℕ∞) 0 y * HPow.hPow (α := ℕ∞) 0 z
have inl : HPow.hPow (α := ℕ∞) 0 (y + z) = 0
Tactic: rw [zero_epow y_0.ne.symm, zero_mul]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z
have inr : x ^ (⊤ + z) = HPow.hPow (β := ℕ∞) x ⊤ * x ^ z
Tactic: induction y
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
inr : x ^ (⊤ + z) = HPow.hPow (β := ℕ∞) x ⊤ * x ^ z
⊢ x ^ (y + z) = x ^ y * x ^ z
have inr₁ : ∀ (a : ℕ), x ^ ((↑a : ℕ∞) + z) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * x ^ z
Tactic: induction y
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (⊤ + z) = HPow.hPow (β := ℕ∞) x ⊤ * x ^ z
have inr : x ^ z ≠ 0
Tactic: rw [top_add, epow_top x_2, top_mul]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
⊢ x ^ ((↑a : ℕ∞) + z) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * x ^ z
have inr : x ^ HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) x ⊤
Tactic: induction z
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
inr : x ^ HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) x ⊤
⊢ x ^ ((↑a : ℕ∞) + z) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * x ^ z
have inr₁ : ∀ (a_1 : ℕ),
  x ^ HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) x (↑a_1 : ℕ∞)
Tactic: induction z
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
⊢ x ^ HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) x ⊤
have inr : HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ≠ 0
Tactic: rw [add_top, epow_top x_2, mul_top]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
⊢ (x * y) ^ z = x ^ z * y ^ z
have top : HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
Tactic: induction z
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
top : HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
⊢ (x * y) ^ z = x ^ z * y ^ z
have coe : ∀ (a : ℕ), HPow.hPow (β := ℕ∞) (x * y) (↑a : ℕ∞) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) y (↑a : ℕ∞)
Tactic: induction z
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
have top : ∀ (x_0 : x < 1), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
top : ∀ (x_0 : x < 1), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
have top₁ : HPow.hPow (β := ℕ∞) (1 * y) ⊤ = HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ * HPow.hPow (β := ℕ∞) y ⊤
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
top : ∀ (x_0 : x < 1), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
top₁ : HPow.hPow (β := ℕ∞) (1 * y) ⊤ = HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ * HPow.hPow (β := ℕ∞) y ⊤
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
have top₂ : ∀ (x_2 : 1 < x), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
have top : ∀ (y_0 : y < 1), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
Tactic: rcases lt_trichotomy y 1 with y_0 | rfl | y_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
top : ∀ (y_0 : y < 1), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
have top₁ : HPow.hPow (β := ℕ∞) (x * 1) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤
Tactic: rcases lt_trichotomy y 1 with y_0 | rfl | y_2
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
top : ∀ (y_0 : y < 1), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
top₁ : HPow.hPow (β := ℕ∞) (x * 1) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
have top₂ : ∀ (y_2 : 1 < y), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
Tactic: rcases lt_trichotomy y 1 with y_0 | rfl | y_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
have top : HPow.hPow (β := ℕ∞) (x * y) ⊤ = ⊤
Tactic: rw [epow_top x_2, epow_top y_2, WithTop.top_mul_top]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
⊢ x ^ (y * z) = (x ^ y) ^ z
have inl : ∀ (y_0 : y = 0), x ^ (y * z) = (x ^ y) ^ z
Tactic: rcases eq_or_ne y 0 with y_0 | y_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
inl : ∀ (y_0 : y = 0), x ^ (y * z) = (x ^ y) ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr : ∀ (y_0 : y ≠ 0), x ^ (y * z) = (x ^ y) ^ z
Tactic: rcases eq_or_ne y 0 with y_0 | y_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr : ∀ (z_0 : z = 0), x ^ (y * z) = (x ^ y) ^ z
Tactic: rcases eq_or_ne z 0 with z_0 | z_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
inr : ∀ (z_0 : z = 0), x ^ (y * z) = (x ^ y) ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr₁ : ∀ (z_0 : z ≠ 0), x ^ (y * z) = (x ^ y) ^ z
Tactic: rcases eq_or_ne z 0 with z_0 | z_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr : ∀ (x_0 : x < 1), x ^ (y * z) = (x ^ y) ^ z
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
inr : ∀ (x_0 : x < 1), x ^ (y * z) = (x ^ y) ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr₁ : HPow.hPow (α := ℕ∞) 1 (y * z) = HPow.hPow (α := ℕ∞) 1 y ^ z
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
inr : ∀ (x_0 : x < 1), x ^ (y * z) = (x ^ y) ^ z
inr₁ : HPow.hPow (α := ℕ∞) 1 (y * z) = HPow.hPow (α := ℕ∞) 1 y ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr₂ : ∀ (x_2 : 1 < x), x ^ (y * z) = (x ^ y) ^ z
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr : HPow.hPow (α := ℕ∞) 0 (y * z) = HPow.hPow (α := ℕ∞) 0 y ^ z
Tactic: rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
inr : HPow.hPow (α := ℕ∞) 0 (y * z) = HPow.hPow (α := ℕ∞) 0 y ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr₁ : HPow.hPow (α := ℕ∞) 0 (y * z) = HPow.hPow (α := ℕ∞) 0 z
Tactic: rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
inr : HPow.hPow (α := ℕ∞) 0 (y * z) = HPow.hPow (α := ℕ∞) 0 y ^ z
inr₁ : HPow.hPow (α := ℕ∞) 0 (y * z) = HPow.hPow (α := ℕ∞) 0 z
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr₂ : HPow.hPow (α := ℕ∞) 0 (y * z) = 0
Tactic: rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
inr : HPow.hPow (α := ℕ∞) 0 (y * z) = HPow.hPow (α := ℕ∞) 0 y ^ z
inr₁ : HPow.hPow (α := ℕ∞) 0 (y * z) = HPow.hPow (α := ℕ∞) 0 z
inr₂ : HPow.hPow (α := ℕ∞) 0 (y * z) = 0
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr₃ : Eq (α := ℕ∞) 0 0
Tactic: rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr : ∀ (y_0 : Ne (α := ℕ∞) ⊤ 0), x ^ (⊤ * z) = HPow.hPow (β := ℕ∞) x ⊤ ^ z
Tactic: induction y
Cleared hypotheses: y_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
inr : ∀ (y_0 : Ne (α := ℕ∞) ⊤ 0), x ^ (⊤ * z) = HPow.hPow (β := ℕ∞) x ⊤ ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z
have inr₁ : ∀ (a : ℕ) (y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0), x ^ ((↑a : ℕ∞) * z) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ^ z
Tactic: induction y
Cleared hypotheses: y_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : Ne (α := ℕ∞) ⊤ 0
⊢ x ^ (⊤ * z) = HPow.hPow (β := ℕ∞) x ⊤ ^ z
have inr : HPow.hPow (β := ℕ∞) x ⊤ = HPow.hPow (β := ℕ∞) x ⊤ ^ z
Tactic: rw [top_mul z_0, epow_top x_2, top_epow z_0]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : Ne (α := ℕ∞) ⊤ 0
inr : HPow.hPow (β := ℕ∞) x ⊤ = HPow.hPow (β := ℕ∞) x ⊤ ^ z
⊢ x ^ (⊤ * z) = HPow.hPow (β := ℕ∞) x ⊤ ^ z
have inr₁ : ⊤ = HPow.hPow (α := ℕ∞) ⊤ z
Tactic: rw [top_mul z_0, epow_top x_2, top_epow z_0]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : Ne (α := ℕ∞) ⊤ 0
inr : HPow.hPow (β := ℕ∞) x ⊤ = HPow.hPow (β := ℕ∞) x ⊤ ^ z
inr₁ : ⊤ = HPow.hPow (α := ℕ∞) ⊤ z
⊢ x ^ (⊤ * z) = HPow.hPow (β := ℕ∞) x ⊤ ^ z
have inr₂ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [top_mul z_0, epow_top x_2, top_epow z_0]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
⊢ x ^ ((↑a : ℕ∞) * z) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ^ z
have inr : ∀ (z_0 : Ne (α := ℕ∞) ⊤ 0),
  x ^ HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) ⊤
Tactic: induction z
Cleared hypotheses: z_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
inr :
  ∀ (z_0 : Ne (α := ℕ∞) ⊤ 0),
    x ^ HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) ⊤
⊢ x ^ ((↑a : ℕ∞) * z) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ^ z
have inr₁ : ∀ (a_1 : ℕ) (z_0 : Ne (α := ℕ∞) (↑a_1 : ℕ∞) 0),
  x ^ HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞) = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) (↑a_1 : ℕ∞)
Tactic: induction z
Cleared hypotheses: z_0
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
z_0 : Ne (α := ℕ∞) ⊤ 0
⊢ x ^ HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) ⊤
have inr : ⊤ = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) ⊤
Tactic: rw [mul_top y_0, epow_top x_2]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
z_0 : Ne (α := ℕ∞) ⊤ 0
⊢ ⊤ = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) ⊤
have apply : 1 < HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)
Tactic: apply (epow_top _).symm
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
z_0 : Ne (α := ℕ∞) ⊤ 0
⊢ 1 < HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)
have apply : LT.lt (α := ℕ∞) 1 ((fun (y : ℕ∞) ↦ x ^ y) 1)
Tactic: apply (epow_right_mono (one_le_iff_ne_zero.1 x_2.le) (one_le_iff_ne_zero.2 y_0)).trans_lt'
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
p : EReal → Prop
r : EReal
hr : p r
⊢ p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
have bot : ∀ (hr : p ⊥), p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
Tactic: cases r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
p : EReal → Prop
r : EReal
hr : p r
bot : ∀ (hr : p ⊥), p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
⊢ p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
have coe : ∀ (a : ℝ) (hr : p (↑a : EReal)), p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
Tactic: cases r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
p : EReal → Prop
r : EReal
hr : p r
bot : ∀ (hr : p ⊥), p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
coe : ∀ (a : ℝ) (hr : p (↑a : EReal)), p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
⊢ p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
have top : ∀ (hr : p ⊤), p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
Tactic: cases r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
⊢ P ⊥ (↑y : EReal)
have inl : ∀ (hy : y < 0), P ⊥ (↑y : EReal)
Tactic: rcases lt_trichotomy y 0 with (hy | rfl | hy)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
inl : ∀ (hy : y < 0), P ⊥ (↑y : EReal)
⊢ P ⊥ (↑y : EReal)
have inr : P ⊥ (↑0 : EReal)
Tactic: rcases lt_trichotomy y 0 with (hy | rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
inl : ∀ (hy : y < 0), P ⊥ (↑y : EReal)
inr : P ⊥ (↑0 : EReal)
⊢ P ⊥ (↑y : EReal)
have inr₁ : ∀ (hy : 0 < y), P ⊥ (↑y : EReal)
Tactic: rcases lt_trichotomy y 0 with (hy | rfl | hy)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
⊢ P (↑x : EReal) ⊥
have inl : ∀ (hx : x < 0), P (↑x : EReal) ⊥
Tactic: rcases lt_trichotomy x 0 with (hx | rfl | hx)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
inl : ∀ (hx : x < 0), P (↑x : EReal) ⊥
⊢ P (↑x : EReal) ⊥
have inr : P (↑0 : EReal) ⊥
Tactic: rcases lt_trichotomy x 0 with (hx | rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
inl : ∀ (hx : x < 0), P (↑x : EReal) ⊥
inr : P (↑0 : EReal) ⊥
⊢ P (↑x : EReal) ⊥
have inr₁ : ∀ (hx : 0 < x), P (↑x : EReal) ⊥
Tactic: rcases lt_trichotomy x 0 with (hx | rfl | hx)
-- Lean 4 proof step from Mathlib.Data.EReal.Basic (goal)
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
⊢ P (↑x : EReal) ⊤
have inl : ∀ (hx : x < 0), P (↑x : EReal) ⊤
Tactic: rcases lt_trichotomy x 0 with (hx | rfl | hx)