awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
have h : (0, (single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0) ∈ CNF b o
Tactic: apply coeff_of_mem_CNF
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (0, (single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0) ∈ CNF b o
have h : Membership.mem (γ := List (Ordinal.{u_1} × Ordinal.{u_1})) [(0, o)]
  (0, (single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
Tactic: rw [CNF.of_le_one hb ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
have h : Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1}) (0 : Ordinal.{u_1})
Tactic: rw [single_eq_of_ne ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1}) (0 : Ordinal.{u_1})
have h : a ∉ map Prod.fst (CNF b o)
Tactic: apply coeff_of_notMem_CNF
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ a ∉ map Prod.fst (CNF b o)
have h : a ∉ map Prod.fst [(0, o)]
Tactic: rw [CNF.of_le_one hb ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ coeff b (b ^ e * x + y) = single e x + coeff b y
have h : ∀ (e' : Ordinal.{u_1}),
  Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((single e x + coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
Tactic: ext e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
⊢ (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' =
    HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
      ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
      ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
have h : (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e =
  HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
    ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
Tactic: obtain rfl | he := eq_or_ne e e'
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
h :
  (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e =
    HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
      ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
      ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
⊢ (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' =
    HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
      ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
      ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
have h₁ : ∀ (he : e ≠ e'),
  (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' =
    HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
      ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
      ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
Tactic: obtain rfl | he := eq_or_ne e e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e =
    HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
      ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
      ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
have h : (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = x
Tactic: rw [single_eq_same, coeff_eq_zero_of_lt hy, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = x
have h : (e, x) ∈ CNF b (b ^ e * x + y)
Tactic: apply coeff_of_mem_CNF
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (e, x) ∈ CNF b (b ^ e * x + y)
have h : (e, x) ∈ (e, x) :: CNF b y
Tactic: rw [CNF.opow_mul_add hb hx hxb hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
⊢ (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' =
    HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
      ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
      ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
have h : Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
  ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
Tactic: rw [single_eq_of_ne' he, zero_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
⊢ Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
have pos : ∀ (h : e' ∈ map Prod.fst (CNF b y)),
  Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
Tactic: by_cases h : e' ∈ (CNF b y).map Prod.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
pos :
  ∀ (h : e' ∈ map Prod.fst (CNF b y)),
    Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
      ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
have neg : ∀ (h : e' ∉ map Prod.fst (CNF b y)),
  Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
Tactic: by_cases h : e' ∈ (CNF b y).map Prod.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (hypothesis)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∈ map Prod.fst (CNF b y)
⊢ Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
have h₁ : ∃ a ∈ CNF b y, a.1 = e'
Tactic: rw [mem_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : ∃ a ∈ CNF b y, a.1 = e'
⊢ Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
have pos : ∀ (f c : Ordinal.{u_1}) (hf : (f, c) ∈ CNF b y) (he : e ≠ (f, c).1),
  Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (f, c).1 : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (f, c).1 : Ordinal.{u_1})
Tactic: obtain ⟨⟨f, c⟩, hf, rfl⟩ := h
Cleared hypotheses: e', he, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (f, c).1 : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (f, c).1 : Ordinal.{u_1})
have pos : (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (f, c).1 = c
Tactic: rw [coeff_of_mem_CNF hf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (f, c).1 = c
have pos : ((f, c).1, c) ∈ CNF b (b ^ e * x + y)
Tactic: apply coeff_of_mem_CNF
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ ((f, c).1, c) ∈ CNF b (b ^ e * x + y)
have pos : ((f, c).1, c) ∈ (e, x) :: CNF b y
Tactic: rw [CNF.opow_mul_add hb hx hxb hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∉ map Prod.fst (CNF b y)
⊢ Eq (α := Ordinal.{u_1}) ((coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((coeff b y : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
have neg : e' ∉ map Prod.fst (CNF b (b ^ e * x + y))
Tactic: rw [coeff_of_notMem_CNF h, coeff_of_notMem_CNF]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∉ map Prod.fst (CNF b y)
⊢ e' ∉ map Prod.fst (CNF b (b ^ e * x + y))
have neg : ∀ (h : ¬∃ a ∈ CNF b y, a.1 = e'), ¬∃ a ∈ CNF b (b ^ e * x + y), a.1 = e'
Tactic: rw [mem_map] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : ¬∃ a ∈ CNF b y, a.1 = e'
⊢ ¬∃ a ∈ CNF b (b ^ e * x + y), a.1 = e'
have neg : ¬∃ a ∈ (e, x) :: CNF b y, a.1 = e'
Tactic: rw [CNF.opow_mul_add hb hx hxb hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
⊢ eval b (single e x + f) = b ^ e * x + eval b f
have inl : eval b (single e 0 + f) = b ^ e * 0 + eval b f
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
inl : eval b (single e 0 + f) = b ^ e * 0 + eval b f
⊢ eval b (single e x + f) = b ^ e * x + eval b f
have inr : ∀ (hx : x ≠ 0), eval b (single e x + f) = b ^ e * x + eval b f
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ Eq (α := Ordinal.{u_1}) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
have rw : e ∉ f.support
Tactic: rw [← notMem_support_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (hypothesis)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ eval b (single e x + f) = b ^ e * x + eval b f
have hf : Eq (α := Ordinal.{u_1}) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
Tactic: have hf : f e = 0 := by
    rw [← notMem_support_iff]
    exact fun he ↦ (h e he).false
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : Eq (α := Ordinal.{u_1}) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
⊢ eval b (single e x + f) = b ^ e * x + eval b f
have inr : foldr
    (fun (p r : Ordinal.{u_1}) ↦
      HMul.hMul (β := Ordinal.{u_1}) (b ^ p)
          ((single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) p : Ordinal.{u_1}) +
        r)
    0 (e :: f.support.sort fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2) =
  b ^ e * x + eval b f
Tactic: rw [eval, support_single_add (by simpa) hx, Finset.sort_cons]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : Eq (α := Ordinal.{u_1}) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
inr :
  foldr
      (fun (p r : Ordinal.{u_1}) ↦
        HMul.hMul (β := Ordinal.{u_1}) (b ^ p)
            ((single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) p : Ordinal.{u_1}) +
          r)
      0 (e :: f.support.sort fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2) =
    b ^ e * x + eval b f
⊢ eval b (single e x + f) = b ^ e * x + eval b f
have inr₁ : ∀ b ∈ f.support, e ≥ b
Tactic: rw [eval, support_single_add (by simpa) hx, Finset.sort_cons]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : Eq (α := Ordinal.{u_1}) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
⊢ foldr
      (fun (p r : Ordinal.{u_1}) ↦
        HMul.hMul (β := Ordinal.{u_1}) (b ^ p)
            ((single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) p : Ordinal.{u_1}) +
          r)
      0 (e :: f.support.sort fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2) =
    b ^ e * x + eval b f
have inr : foldr
    (fun (p r : Ordinal.{u_1}) ↦
      b ^ p *
          HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
            ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) p : Ordinal.{u_1})
            ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) p : Ordinal.{u_1}) +
        r)
    0 (f.support.sort fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2) =
  eval b f
Tactic: simp only [add_apply, foldr_cons, single_eq_same, hf, add_zero, add_right_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : Eq (α := Ordinal.{u_1}) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
⊢ foldr
      (fun (p r : Ordinal.{u_1}) ↦
        b ^ p *
            HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
              ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) p : Ordinal.{u_1})
              ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) p : Ordinal.{u_1}) +
          r)
      0 (f.support.sort fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2) =
    eval b f
have inr : ∀ a ∈ f.support.sort fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2,
  ∀ (b_1 : Ordinal.{u_1}),
    b ^ a *
          HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
            ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
            ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1}) +
        b_1 =
      HMul.hMul (β := Ordinal.{u_1}) (b ^ a) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1}) + b_1
Tactic: apply foldr_ext
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : Eq (α := Ordinal.{u_1}) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2
b_1 : Ordinal.{u_1}
⊢ b ^ e' *
        HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
          ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
          ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1}) +
      b_1 =
    HMul.hMul (β := Ordinal.{u_1}) (b ^ e') ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1}) + b_1
have inr : HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
    ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1}) =
  (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e'
Tactic: congr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : Eq (α := Ordinal.{u_1}) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2
b_1 : Ordinal.{u_1}
⊢ HAdd.hAdd (α := Ordinal.{u_1}) (β := Ordinal.{u_1})
      ((single e x : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
      ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1}) =
    (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e'
have inr : e' ≠ e
Tactic: rw [single_eq_of_ne, zero_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
h_1 : ∀ (h : single e' y + f = f), eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
⊢ eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
have single_add : ∀ (h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e'),
  (∀ (h : single e' y + f = f), eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)) →
    eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)
Tactic: obtain rfl | he' := (h e' (by simp [hy])).eq_or_lt
Cleared hypotheses: e, h, h_1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
h_1 : ∀ (h : single e' y + f = f), eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
single_add :
  ∀ (h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e'),
    (∀ (h : single e' y + f = f), eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)) →
      eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)
⊢ eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
have single_add₁ : ∀ (he' : e' < e), eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
Tactic: obtain rfl | he' := (h e' (by simp [hy])).eq_or_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
h_1 : ∀ (h : single e' y + f = f), eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
he' : e' < e
⊢ eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
have single_add : ∀ e'_1 ∈ (single e' y + f).support, e'_1 < e
Tactic: rw [eval_single_add']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
h_1 : ∀ (h : single e' y + f = f), eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
he' : e' < e
⊢ ∀ e'_1 ∈ (single e' y + f).support, e'_1 < e
have single_add : ∀ (a : Ordinal.{u_1}) (ha : a ∈ (single e' y + f).support), a ≠ e
Tactic: refine fun a ha ↦ (h a ha).lt_of_ne ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
a : Ordinal.{u_1}
ha : a ∈ (single e' y + f).support
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ a
h_1 : ∀ (h : single e' y + f = f), eval b (single a x + (single e' y + f)) = b ^ a * x + eval b (single e' y + f)
he' : e' < a
⊢ False
have apply : a ∈ f.support
Tactic: apply (hf a _).not_gt he'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' ≤ e
⊢ eval b (single e x + f) = b ^ e * x + eval b f
have zero : ∀ (h : ∀ (e' : Ordinal.{u_1}), Membership.mem (γ := Finset Ordinal.{u_1}) (support (M := Ordinal.{u_1}) 0) e' → e' ≤ e),
  eval b (HAdd.hAdd (α := Ordinal.{u_1} →₀ Ordinal.{u_1}) (single e x) 0) = b ^ e * x + eval b 0
Tactic: cases f using Finsupp.induction_on_max with
  | zero => simp
  | single_add e' y f hf hy =>
    obtain rfl | he' := (h e' (by simp [hy])).eq_or_lt
    · simp only [← add_assoc, ← single_add, eval_single_add' _ hf, mul_add]
    · rw [eval_single_add']
      refine fun a ha ↦ (h a ha).lt_of_ne ?_
      rintro rfl
      apply (hf a _).not_gt he'
      simpa [he'.ne'] using ha
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' ≤ e
zero :
  ∀
    (h :
      ∀ (e' : Ordinal.{u_1}), Membership.mem (γ := Finset Ordinal.{u_1}) (support (M := Ordinal.{u_1}) 0) e' → e' ≤ e),
    eval b (HAdd.hAdd (α := Ordinal.{u_1} →₀ Ordinal.{u_1}) (single e x) 0) = b ^ e * x + eval b 0
⊢ eval b (single e x + f) = b ^ e * x + eval b f
have single_add : ∀ (e' y : Ordinal.{u_1}) (f : Ordinal.{u_1} →₀ Ordinal.{u_1}) (hf : ∀ c ∈ f.support, c < e') (hy : y ≠ 0)
  (h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e),
  (∀ (h : single e' y + f = f), eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)) →
    eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
Tactic: cases f using Finsupp.induction_on_max with
  | zero => simp
  | single_add e' y f hf hy =>
    obtain rfl | he' := (h e' (by simp [hy])).eq_or_lt
    · simp only [← add_assoc, ← single_add, eval_single_add' _ hf, mul_add]
    · rw [eval_single_add']
      refine fun a ha ↦ (h a ha).lt_of_ne ?_
      rintro rfl
      apply (hf a _).not_gt he'
      simpa [he'.ne'] using ha
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : ∀ (h : ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁), eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ eval b (single e₁ x + f₁ + f₂) = eval b (single e₁ x + f₁) + eval b f₂
have single_add : ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
Tactic: rw [add_assoc, eval_single_add, eval_single_add' _ hf₁, IH, add_assoc]