awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
inl : HAdd.hAdd (α := ℕ∞) ⊤ (⨆ (i : ι), f i) = ⨆ (i : ι), ⊤ + f i
⊢ a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
have inr : ∀ (ha : a ≠ ⊤), a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
Tactic: obtain rfl | ha := eq_or_ne a ⊤
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
i : ι
⊢ a + f i ≤ a + ⨆ (i : ι), f i
have grw : a + f i ≤ a + f i
Tactic: grw [← le_iSup]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
have inr : a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i
Tactic: refine le_antisymm ?_ <| iSup_le fun i ↦ by grw [← le_iSup]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i
have inr : ⨆ (i : ι), f i ≤ (⨆ (i : ι), a + f i) - a
Tactic: refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (hypothesis)
Goal:
ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ (i : ι), p i
f : ι → ℕ∞
⊢ a + ⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), a + f i
have this : Nonempty.{max 1 u_2} { i : ι // p i }
Tactic: haveI : Nonempty {i // p i} := nonempty_subtype.2 h
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ a + sSup s = ⨆ b ∈ s, a + b
have rw : a + ⨆ a ∈ s, a = ⨆ b ∈ s, a + b
Tactic: rw [sSup_eq_iSup, add_biSup hs]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
rw : a + ⨆ a ∈ s, a = ⨆ b ∈ s, a + b
⊢ a + sSup s = ⨆ b ∈ s, a + b
have rw₁ : Eq (α := ℕ∞) (⨆ i ∈ s, a + i) (⨆ b ∈ s, a + b)
Tactic: rw [sSup_eq_iSup, add_biSup hs]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ sSup s + a = ⨆ b ∈ s, b + a
have rw : (⨆ a ∈ s, a) + a = ⨆ b ∈ s, b + a
Tactic: rw [sSup_eq_iSup, biSup_add hs]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
rw : (⨆ a ∈ s, a) + a = ⨆ b ∈ s, b + a
⊢ sSup s + a = ⨆ b ∈ s, b + a
have rw₁ : Eq (α := ℕ∞) (⨆ i ∈ s, i + a) (⨆ b ∈ s, b + a)
Tactic: rw [sSup_eq_iSup, biSup_add hs]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
inst_1 : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a
have simp_rw : ⨆ (i : ι), ⨆ (i_1 : κ), f i + g i_1 ≤ a
Tactic: simp_rw [iSup_add, add_iSup]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ (i : ι), p i
hq : ∃ (j : κ), q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ HAdd.hAdd (α := ℕ∞) (⨆ (i : ι), ⨆ (_ : p i), f i) (⨆ (j : κ), ⨆ (_ : q j), g j) ≤ a
have simp_rw : ⨆ (i : ι), ⨆ (_ : p i), ⨆ (i_1 : κ), ⨆ (_ : q i_1), f i + g i_1 ≤ a
Tactic: simp_rw [biSup_add' hp, add_biSup' hq]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i
have inl : IsEmpty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
inl : IsEmpty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i
have inr : Nonempty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i
have inr : iSup f + iSup g ≤ ⨆ (i : ι), f i + g i
Tactic: refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ (i : ι), f i + g i
have inr : ∀ (i j : ι), f i + g j ≤ ⨆ (i : ι), f i + g i
Tactic: refine iSup_add_iSup_le fun i j => ?_
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
i j : ι
⊢ f i + g j ≤ ⨆ (i : ι), f i + g i
have inr : ∀ (k : ι) (hk : f i + g j ≤ f k + g k), f i + g j ≤ ⨆ (i : ι), f i + g i
Tactic: rcases h i j with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i + g j ≤ f _k + g _k
have h₁ : f i ≤ f _k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
h₁ : f i ≤ f _k
⊢ f i + g j ≤ f _k + g _k
have h₂ : g j ≤ g _k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
R : Type u_4
inst : SMul R ℕ∞
inst_1 : IsScalarTower R ℕ∞ ℕ∞
s : Set ℕ∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a
have simp_rw : HSMul.hSMul (β := ℕ∞) c (⨆ a ∈ s, a) = ⨆ a ∈ s, c • a
Tactic: simp_rw [sSup_eq_iSup, smul_iSup]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have inl : ∀ (i : ι) (hi : a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
Tactic: obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
inl : ∀ (i : ι) (hi : a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have inr : ∀ (h : ¬∃ (i : ι), a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
Tactic: obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have inl : ∀ (b : ℕ∞), ⊥ < b → ∃ (i : ι), a - f i < b
Tactic: rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, iInf_eq_bot.2, bot_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (hypothesis)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ (i : ι), a < f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have h₁ : ∀ (x : ι), f x ≤ a
Tactic: simp_rw [not_exists, not_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
have inr : ∀ (i : ι), f i ≤ a - ⨅ (i : ι), a - f i
Tactic: refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
    ENat.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
    add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
    iSup_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ f i ≤ a - ⨅ (i : ι), a - f i
have inr : a - (a - f i) ≤ a - ⨅ (i : ι), a - f i
Tactic: rw [← ENat.sub_sub_cancel ha (h _)]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i
have refine : ∀ (c : ℕ∞), a - ⨅ (i : ι), f i ≤ c ↔ ⨆ (i : ι), a - f i ≤ c
Tactic: refine eq_of_forall_ge_iff fun c => ?_
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a c : ℕ∞
⊢ a - ⨅ (i : ι), f i ≤ c ↔ ⨆ (i : ι), a - f i ≤ c
have rw : a ≤ ⨅ (i : ι), f i + c ↔ ⨆ (i : ι), a - f i ≤ c
Tactic: rw [tsub_le_iff_right, add_comm, iInf_add]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a + iInf f = ⨅ (b : ι), a + f b
have rw : Eq (α := ℕ∞) (⨅ (i : ι), f i + a) (⨅ (b : ι), a + f b)
Tactic: rw [add_comm, iInf_add]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f k + g k ≤ f i + g j
⊢ ⨅ (a : ι), ⨅ (a' : ι), f a + g a' = iInf f + iInf g
have simp_rw : Eq (α := ℕ∞) (⨅ (a : ι), ⨅ (a' : ι), f a + g a') (⨅ (i : ι), f i + iInf g)
Tactic: simp_rw [iInf_add, add_iInf]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k + g _k ≤ f i + g j
have h₁ : f _k ≤ f i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
h₁ : f _k ≤ f i
⊢ f _k + g _k ≤ f i + g j
have h₂ : g _k ≤ g j
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
a : ℕ∞
s : Set ℕ∞
⊢ a + sInf s = ⨅ b ∈ s, a + b
have rw : a + ⨅ a ∈ s, a = ⨅ b ∈ s, a + b
Tactic: rw [sInf_eq_iInf, add_iInf₂]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
a : ℕ∞
s : Set ℕ∞
rw : a + ⨅ a ∈ s, a = ⨅ b ∈ s, a + b
⊢ a + sInf s = ⨅ b ∈ s, a + b
have rw₁ : Eq (α := ℕ∞) (⨅ i ∈ s, a + i) (⨅ b ∈ s, a + b)
Tactic: rw [sInf_eq_iInf, add_iInf₂]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g
have simp_rw : a ≤ ⨅ (i : ι), ⨅ (b : κ), f i + g b
Tactic: simp_rw [iInf_add, add_iInf]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ HAdd.hAdd (α := ℕ∞) (⨅ (i : ι), ⨅ (qi : q₁ i), f i qi) (⨅ (k : κ), ⨅ (qk : q₂ k), g k qk)
have simp_rw : a ≤ ⨅ (i : ι), ⨅ (j : q₁ i), ⨅ (i_1 : κ), ⨅ (j_1 : q₂ i_1), f i j + g i_1 j_1
Tactic: simp_rw [iInf₂_add, add_iInf₂]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
⊢ HPow.hPow (β := ℕ∞) x ⊤ = if LT.lt (α := ℕ∞) ⊤ ⊤ then x ^ toNat ⊤ else if x = 0 then 0 else if x = 1 then 1 else ⊤
have top : HPow.hPow (β := ℕ∞) x ⊤ = if x = 0 then 0 else if x = 1 then 1 else ⊤
Tactic: simp only [lt_self_iff_false, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
n : ℕ
⊢ HPow.hPow (β := ℕ∞) x (↑n : ℕ∞) =
    if LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤ then x ^ toNat (↑n : ℕ∞) else if x = 0 then 0 else if x = 1 then 1 else ⊤
have coe : HPow.hPow (β := ℕ∞) x (↑n : ℕ∞) = x ^ n
Tactic: simp only [coe_lt_top, ↓reduceIte, toNat_coe]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
⊢ x ^ y = if y < ⊤ then x ^ y.toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤
have top : HPow.hPow (β := ℕ∞) x ⊤ = if LT.lt (α := ℕ∞) ⊤ ⊤ then x ^ toNat ⊤ else if x = 0 then 0 else if x = 1 then 1 else ⊤
Tactic: cases y with
  | top => simp only [lt_self_iff_false, ↓reduceIte]; rfl
  | coe n => simp only [coe_lt_top, ↓reduceIte, toNat_coe]; rfl
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x y : ℕ∞
top : HPow.hPow (β := ℕ∞) x ⊤ = if LT.lt (α := ℕ∞) ⊤ ⊤ then x ^ toNat ⊤ else if x = 0 then 0 else if x = 1 then 1 else ⊤
⊢ x ^ y = if y < ⊤ then x ^ y.toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤
have coe : ∀ (n : ℕ),
  HPow.hPow (β := ℕ∞) x (↑n : ℕ∞) =
    if LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤ then x ^ toNat (↑n : ℕ∞) else if x = 0 then 0 else if x = 1 then 1 else ⊤
Tactic: cases y with
  | top => simp only [lt_self_iff_false, ↓reduceIte]; rfl
  | coe n => simp only [coe_lt_top, ↓reduceIte, toNat_coe]; rfl
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 (↑y : ℕ∞) = 0
have coe : HPow.hPow (α := ℕ∞) 0 y = 0
Tactic: rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
coe : HPow.hPow (α := ℕ∞) 0 y = 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 (↑y : ℕ∞) = 0
have coe₁ : Eq (α := ℕ∞) 0 0 ∧ y ≠ 0
Tactic: rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
coe : HPow.hPow (α := ℕ∞) 0 y = 0
coe₁ : Eq (α := ℕ∞) 0 0 ∧ y ≠ 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 (↑y : ℕ∞) = 0
have coe₂ : True ∧ y ≠ 0
Tactic: rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
coe : HPow.hPow (α := ℕ∞) 0 y = 0
coe₁ : Eq (α := ℕ∞) 0 0 ∧ y ≠ 0
coe₂ : True ∧ y ≠ 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 (↑y : ℕ∞) = 0
have coe₃ : y ≠ 0
Tactic: rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y : ℕ∞
h : y ≠ 0
⊢ HPow.hPow (α := ℕ∞) 0 y = 0
have top : ∀ (h : Ne (α := ℕ∞) ⊤ 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 ⊤ = 0
Tactic: induction y with
  | top => exact zero_epow_top
  | coe y => rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y : ℕ∞
h : y ≠ 0
top : ∀ (h : Ne (α := ℕ∞) ⊤ 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 ⊤ = 0
⊢ HPow.hPow (α := ℕ∞) 0 y = 0
have coe : ∀ (y : ℕ) (h : Ne (α := ℕ∞) (↑y : ℕ∞) 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 (↑y : ℕ∞) = 0
Tactic: induction y with
  | top => exact zero_epow_top
  | coe y => rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 (↑y : ℕ∞) = 1
have coe : HPow.hPow (α := ℕ∞) 1 y = 1
Tactic: rw [epow_natCast, one_pow]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
coe : HPow.hPow (α := ℕ∞) 1 y = 1
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 (↑y : ℕ∞) = 1
have coe₁ : Eq (α := ℕ∞) 1 1
Tactic: rw [epow_natCast, one_pow]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y : ℕ∞
⊢ HPow.hPow (α := ℕ∞) 1 y = 1
have top : HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ = 1
Tactic: induction y with
  | top => rfl
  | coe y => rw [epow_natCast, one_pow]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y : ℕ∞
top : HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ = 1
⊢ HPow.hPow (α := ℕ∞) 1 y = 1
have coe : ∀ (y : ℕ), HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 (↑y : ℕ∞) = 1
Tactic: induction y with
  | top => rfl
  | coe y => rw [epow_natCast, one_pow]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ (↑y : ℕ∞) = ⊤
have coe : HPow.hPow (α := ℕ∞) ⊤ y = ⊤
Tactic: rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
coe : HPow.hPow (α := ℕ∞) ⊤ y = ⊤
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ (↑y : ℕ∞) = ⊤
have coe₁ : Eq (α := ℕ∞) ⊤ ⊤ ∧ y ≠ 0
Tactic: rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
coe : HPow.hPow (α := ℕ∞) ⊤ y = ⊤
coe₁ : Eq (α := ℕ∞) ⊤ ⊤ ∧ y ≠ 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ (↑y : ℕ∞) = ⊤
have coe₂ : True ∧ y ≠ 0
Tactic: rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
coe : HPow.hPow (α := ℕ∞) ⊤ y = ⊤
coe₁ : Eq (α := ℕ∞) ⊤ ⊤ ∧ y ≠ 0
coe₂ : True ∧ y ≠ 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ (↑y : ℕ∞) = ⊤
have coe₃ : y ≠ 0
Tactic: rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y : ℕ∞
h : y ≠ 0
⊢ HPow.hPow (α := ℕ∞) ⊤ y = ⊤
have top : ∀ (h : Ne (α := ℕ∞) ⊤ 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ ⊤ = ⊤
Tactic: induction y with
  | top => exact top_epow_top
  | coe y => rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y : ℕ∞
h : y ≠ 0
top : ∀ (h : Ne (α := ℕ∞) ⊤ 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ ⊤ = ⊤
⊢ HPow.hPow (α := ℕ∞) ⊤ y = ⊤
have coe : ∀ (y : ℕ) (h : Ne (α := ℕ∞) (↑y : ℕ∞) 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ (↑y : ℕ∞) = ⊤
Tactic: induction y with
  | top => exact top_epow_top
  | coe y => rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
⊢ HPow.hPow (β := ℕ∞) x 0 = 1
have rw : HPow.hPow (β := ℕ∞) x (↑0 : ℕ∞) = 1
Tactic: rw [← coe_zero, epow_natCast, pow_zero]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
rw : HPow.hPow (β := ℕ∞) x (↑0 : ℕ∞) = 1
⊢ HPow.hPow (β := ℕ∞) x 0 = 1
have rw₁ : HPow.hPow (β := ℕ) x 0 = 1
Tactic: rw [← coe_zero, epow_natCast, pow_zero]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
rw : HPow.hPow (β := ℕ∞) x (↑0 : ℕ∞) = 1
rw₁ : HPow.hPow (β := ℕ) x 0 = 1
⊢ HPow.hPow (β := ℕ∞) x 0 = 1
have rw₂ : Eq (α := ℕ∞) 1 1
Tactic: rw [← coe_zero, epow_natCast, pow_zero]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
⊢ HPow.hPow (β := ℕ∞) x 1 = x
have rw : HPow.hPow (β := ℕ∞) x (↑1 : ℕ∞) = x
Tactic: rw [← coe_one, epow_natCast, pow_one]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
rw : HPow.hPow (β := ℕ∞) x (↑1 : ℕ∞) = x
⊢ HPow.hPow (β := ℕ∞) x 1 = x
have rw₁ : HPow.hPow (β := ℕ) x 1 = x
Tactic: rw [← coe_one, epow_natCast, pow_one]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
rw : HPow.hPow (β := ℕ∞) x (↑1 : ℕ∞) = x
rw₁ : HPow.hPow (β := ℕ) x 1 = x
⊢ HPow.hPow (β := ℕ∞) x 1 = x
have rw₂ : x = x
Tactic: rw [← coe_one, epow_natCast, pow_one]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (hypothesis)
Goal:
x : ℕ∞
h : 1 < x
⊢ HPow.hPow (β := ℕ∞) x ⊤ = ⊤
have this : LE.le (α := ℕ∞) 0 1
Tactic: have : (0 : ℕ∞) ≤ 1 := zero_le_one
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
h : 1 < x
this : LE.le (α := ℕ∞) 0 1
⊢ HPow.hPow (β := ℕ∞) x ⊤ = ⊤
have hnc : ¬x = 1
Tactic: rw [epow_def, if_neg, if_neg, if_neg]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
h : 1 < x
this : LE.le (α := ℕ∞) 0 1
hnc : ¬x = 1
⊢ HPow.hPow (β := ℕ∞) x ⊤ = ⊤
have hnc₁ : ¬x = 0
Tactic: rw [epow_def, if_neg, if_neg, if_neg]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
h : 1 < x
this : LE.le (α := ℕ∞) 0 1
hnc : ¬x = 1
hnc₁ : ¬x = 0
⊢ HPow.hPow (β := ℕ∞) x ⊤ = ⊤
have hnc₂ : ¬LT.lt (α := ℕ∞) ⊤ ⊤
Tactic: rw [epow_def, if_neg, if_neg, if_neg]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
h : x ≠ 0
y z : ℕ∞
y_z : y ≤ z
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) y) ((fun (y : ℕ∞) ↦ x ^ y) z)
have top : ∀ (y_z : ⊤ ≤ z), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) ⊤) ((fun (y : ℕ∞) ↦ x ^ y) z)
Tactic: induction y
Cleared hypotheses: y, y_z
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
h : x ≠ 0
y z : ℕ∞
y_z : y ≤ z
top : ∀ (y_z : ⊤ ≤ z), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) ⊤) ((fun (y : ℕ∞) ↦ x ^ y) z)
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) y) ((fun (y : ℕ∞) ↦ x ^ y) z)
have coe : ∀ (a : ℕ) (y_z : (↑a : ℕ∞) ≤ z), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) z)
Tactic: induction y
Cleared hypotheses: y, y_z
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
h : x ≠ 0
z : ℕ∞
y_z : ⊤ ≤ z
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) ⊤) ((fun (y : ℕ∞) ↦ x ^ y) z)
have top : LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) ⊤) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
Tactic: rw [top_le_iff.1 y_z]
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
h : x ≠ 0
z : ℕ∞
a : ℕ
y_z : (↑a : ℕ∞) ≤ z
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) z)
have coe : ∀ (y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
Tactic: induction z
Cleared hypotheses: z, y_z
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
h : x ≠ 0
z : ℕ∞
a : ℕ
y_z : (↑a : ℕ∞) ≤ z
coe :
  ∀ (y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) z)
have coe₁ : ∀ (a_1 : ℕ) (y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)),
  LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) (↑a_1 : ℕ∞))
Tactic: induction z
Cleared hypotheses: z, y_z
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
x : ℕ∞
h : x ≠ 0
a : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
have coe : ∀ (x_0 : x < 1), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ 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 : ℕ∞
h : x ≠ 0
a : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤
coe : ∀ (x_0 : x < 1), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
have coe₁ : ∀ (h : Ne (α := ℕ∞) 1 0),
  LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ HPow.hPow (α := ℕ∞) 1 y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ HPow.hPow (α := ℕ∞) 1 y) ⊤)
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 : ℕ∞
h : x ≠ 0
a : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤
coe : ∀ (x_0 : x < 1), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
coe₁ :
  ∀ (h : Ne (α := ℕ∞) 1 0),
    LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ HPow.hPow (α := ℕ∞) 1 y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ HPow.hPow (α := ℕ∞) 1 y) ⊤)
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
have coe₂ : ∀ (x_2 : 1 < x), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y x z : ℕ∞
x_z : x ≤ z
⊢ x ^ y ≤ z ^ y
have top : HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
Tactic: induction y
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y x z : ℕ∞
x_z : x ≤ z
top : HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
⊢ x ^ y ≤ z ^ y
have coe : ∀ (a : ℕ), HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ≤ HPow.hPow (β := ℕ∞) z (↑a : ℕ∞)
Tactic: induction y
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y x z : ℕ∞
x_z : x ≤ z
⊢ HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
have top : ∀ (x_0 : x < 1), HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y x z : ℕ∞
x_z : x ≤ z
top : ∀ (x_0 : x < 1), HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
⊢ HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
have top₁ : ∀ (x_z : 1 ≤ z), HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2
Cleared hypotheses: x, x_z
-- Lean 4 proof step from Mathlib.Data.ENat.Pow (goal)
Goal:
y x z : ℕ∞
x_z : x ≤ z
top : ∀ (x_0 : x < 1), HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
top₁ : ∀ (x_z : 1 ≤ z), HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
⊢ HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
have top₂ : ∀ (x_2 : 1 < x), HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
Tactic: rcases lt_trichotomy x 1 with x_0 | rfl | x_2