awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
h₁ : ∀ (he : (0, c) ∈ CNF b o) (h : o < HPow.hPow (β := Ordinal.{u_1}) b (0, c).1), False
h₂ : ∀ (he' : e ≠ 0), False
⊢ False

Tactic:
obtain rfl | he' := eq_or_ne e 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o c : Ordinal.{u_1}
he : (0, c) ∈ CNF b o
h : o < HPow.hPow (β := Ordinal.{u_1}) b (0, c).1
⊢ False

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
he' : e ≠ 0
⊢ False

Tactic:
(opow_le_of_le_log he' (fst_le_log he)).not_gt h

Premises used: LE.le.not_gt, Ordinal.CNF.fst_le_log, Ordinal.opow_le_of_le_log
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
he' : e ≠ 0
⊢ False

Tactic:
exact (opow_le_of_le_log he' (fst_le_log he)).not_gt h

Premises used: LE.le.not_gt, Ordinal.CNF.fst_le_log, Ordinal.opow_le_of_le_log
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b 0)
⊢ Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})

Tactic:
apply coeff_of_notMem_CNF

Premises used: Ordinal.CNF.coeff_of_notMem_CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e : Ordinal.{u_1}
⊢ e ∉ map Prod.fst (CNF b 0)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
h :
  ∀ (e : Ordinal.{u_1}),
    Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
      ((0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
⊢ coeff b 0 = 0

Tactic:
ext e
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e : Ordinal.{u_1}
⊢ Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
    ((0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})

Tactic:
coeff_zero_apply b e

Premises used: Ordinal.CNF.coeff_zero_apply
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e : Ordinal.{u_1}
⊢ Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
    ((0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})

Tactic:
exact coeff_zero_apply b e

Premises used: Ordinal.CNF.coeff_zero_apply
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
h :
  ∀ (a : Ordinal.{u_1}),
    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})
⊢ coeff b o = single 0 o

Tactic:
ext a
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
h :
  Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
h₁ :
  ∀ (ho : o ≠ 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})
⊢ 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})

Tactic:
obtain rfl | ho := eq_or_ne o 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
a : Ordinal.{u_1}
⊢ Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
h :
  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)
h₁ :
  ∀ (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})
⊢ 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})

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
h : (0, (single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0) ∈ CNF b o
⊢ 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)

Tactic:
apply coeff_of_mem_CNF

Premises used: Ordinal.CNF.coeff_of_mem_CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
h :
  Membership.mem (γ := List (Ordinal.{u_1} × Ordinal.{u_1})) [(0, o)]
    (0, (single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
⊢ (0, (single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0) ∈ CNF b o

Tactic:
rw [CNF.of_le_one hb ho]

Premises used: Ordinal.CNF.of_le_one
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ Membership.mem (γ := List (Ordinal.{u_1} × Ordinal.{u_1})) [(0, o)]
    (0, (single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
h : Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1}) (0 : Ordinal.{u_1})
⊢ 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})

Tactic:
rw [single_eq_of_ne ha]

Premises used: Finsupp.single_eq_of_ne
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
h : a ∉ map Prod.fst (CNF b o)
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1}) (0 : Ordinal.{u_1})

Tactic:
apply coeff_of_notMem_CNF

Premises used: Ordinal.CNF.coeff_of_notMem_CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
h : a ∉ map Prod.fst [(0, o)]
⊢ a ∉ map Prod.fst (CNF b o)

Tactic:
rw [CNF.of_le_one hb ho]

Premises used: Ordinal.CNF.of_le_one
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ a ∉ map Prod.fst [(0, o)]

Tactic:
simpa using ha
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
o : Ordinal.{u_1}
⊢ coeff 0 o = single 0 o

Tactic:
coeff_of_le_one zero_le_one o

Premises used: zero_le_one, Ordinal.CNF.coeff_of_le_one
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
o : Ordinal.{u_1}
⊢ coeff 1 o = single 0 o

Tactic:
coeff_of_le_one le_rfl o

Premises used: le_rfl, Ordinal.CNF.coeff_of_le_one
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
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})
⊢ coeff b (b ^ e * x + y) = single e x + coeff b y

Tactic:
ext e'
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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})
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})
⊢ (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'

Premises used: eq_or_ne, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
h : (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = x
⊢ (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:
rw [single_eq_same, coeff_eq_zero_of_lt hy, add_zero]

Premises used: Finsupp.single_eq_same, Ordinal.CNF.coeff_eq_zero_of_lt, add_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
h : (e, x) ∈ CNF b (b ^ e * x + y)
⊢ (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = x

Tactic:
apply coeff_of_mem_CNF

Premises used: Ordinal.CNF.coeff_of_mem_CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
h : (e, x) ∈ (e, x) :: CNF b y
⊢ (e, x) ∈ CNF b (b ^ e * x + y)

Tactic:
rw [CNF.opow_mul_add hb hx hxb hy]

Premises used: Ordinal.CNF.opow_mul_add
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (e, x) ∈ (e, x) :: CNF b y

Tactic:
mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (e, x) ∈ (e, x) :: CNF b y

Tactic:
exact mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 :
  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})
⊢ (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:
rw [single_eq_of_ne' he, zero_add]

Premises used: Finsupp.single_eq_of_ne', zero_add
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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})
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})
⊢ 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

Premises used: List.map, Prod.fst, Ordinal.CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)
⊢ ∃ a ∈ CNF b y, a.1 = e'

Tactic:
rw [mem_map] at h

Premises used: List.mem_map
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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'
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})
⊢ 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:
obtain ⟨⟨f, c⟩, hf, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
pos : (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (f, c).1 = c
⊢ 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:
rw [coeff_of_mem_CNF hf]

Premises used: Ordinal.CNF.coeff_of_mem_CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
pos : ((f, c).1, c) ∈ CNF b (b ^ e * x + y)
⊢ (coeff b (b ^ e * x + y) : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (f, c).1 = c

Tactic:
apply coeff_of_mem_CNF

Premises used: Ordinal.CNF.coeff_of_mem_CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
pos : ((f, c).1, c) ∈ (e, x) :: CNF b y
⊢ ((f, c).1, c) ∈ CNF b (b ^ e * x + y)

Tactic:
rw [CNF.opow_mul_add hb hx hxb hy]

Premises used: Ordinal.CNF.opow_mul_add
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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) ∈ (e, x) :: CNF b y

Tactic:
mem_cons_of_mem _ hf

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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) ∈ (e, x) :: CNF b y

Tactic:
exact mem_cons_of_mem _ hf

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)
neg : e' ∉ map Prod.fst (CNF b (b ^ e * x + 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:
rw [coeff_of_notMem_CNF h, coeff_of_notMem_CNF]

Premises used: Ordinal.CNF.coeff_of_notMem_CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)
neg : ∀ (h : ¬∃ a ∈ CNF b y, a.1 = e'), ¬∃ a ∈ CNF b (b ^ e * x + y), a.1 = e'
⊢ e' ∉ map Prod.fst (CNF b (b ^ e * x + y))

Tactic:
rw [mem_map] at h ⊢

Premises used: List.mem_map
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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'
neg : ¬∃ a ∈ (e, x) :: CNF b y, a.1 = e'
⊢ ¬∃ a ∈ CNF b (b ^ e * x + y), a.1 = e'

Tactic:
rw [CNF.opow_mul_add hb hx hxb hy]

Premises used: Ordinal.CNF.opow_mul_add
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 ∈ (e, x) :: CNF b y, a.1 = e'

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
⊢ eval b 0 = 0

Tactic:
simp [eval]

Premises used: Ordinal.CNF.eval
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
inr : ∀ (hx : x ≠ 0), eval b (single e x + f) = b ^ e * x + eval b f
⊢ eval b (single e x + f) = b ^ e * x + eval b f

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
⊢ eval b (single e 0 + f) = b ^ e * 0 + eval b f

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
rw : e ∉ f.support
⊢ Eq (α := Ordinal.{u_1}) ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})

Tactic:
rw [← notMem_support_iff]

Premises used: Finsupp.notMem_support_iff
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ e ∉ f.support

Tactic:
fun he ↦ (h e he).false

Premises used: LT.lt.false, Not
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ e ∉ f.support

Tactic:
exact fun he ↦ (h e he).false

Premises used: LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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})

Tactic:
have hf : f e = 0 := by
    rw [← notMem_support_iff]
    exact fun he ↦ (h e he).false
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 ∉ f.support

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
inr₁ : ∀ b ∈ f.support, e ≥ b
⊢ eval b (single e x + f) = b ^ e * x + eval b f

Tactic:
rw [eval, support_single_add (by simpa) hx, Finset.sort_cons]

Premises used: Ordinal.CNF.eval, Finsupp.support_single_add, Finset.sort_cons
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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}) ↦
        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
⊢ 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:
simp only [add_apply, foldr_cons, single_eq_same, hf, add_zero, add_right_inj]

Premises used: Finsupp.single_eq_same, List.foldr_cons, Finsupp.add_apply, add_zero, add_right_inj
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 :
  ∀ 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
⊢ 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:
apply foldr_ext

Premises used: List.foldr_ext
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
inr :
  ∀ (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
⊢ ∀ (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

Tactic:
_
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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}
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'
⊢ 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

Tactic:
congr