awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH :
  ∀ {e : Ordinal.{u_1}} (hb : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b)
    (he : ∀ e' ∈ f.support, e' < e), eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
a : Ordinal.{u_1}
ha : a ∉ f.support
⊢ 0 < b

Tactic:
(hb 0).pos

Premises used: LT.lt.pos, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH :
  ∀ {e : Ordinal.{u_1}} (hb : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b)
    (he : ∀ e' ∈ f.support, e' < e), eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
a : Ordinal.{u_1}
ha : a ∉ f.support
⊢ 0 < b

Tactic:
exact (hb 0).pos

Premises used: LT.lt.pos, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hb : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
he : ∀ e' ∈ f.support, e' < e
zero :
  ∀ {e : Ordinal.{u_1}} (hb : ∀ (e' : Ordinal.{u_1}), (0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b)
    (he :
      ∀ (e' : Ordinal.{u_1}), Membership.mem (γ := Finset Ordinal.{u_1}) (support (M := Ordinal.{u_1}) 0) e' → e' < e),
    eval b 0 < b ^ e
single_add :
  ∀ (e' x : Ordinal.{u_1}) (f : Ordinal.{u_1} →₀ Ordinal.{u_1}) (hf : ∀ c ∈ f.support, c < e') (hx : x ≠ 0)
    (IH :
      ∀ {e : Ordinal.{u_1}} (hb : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b)
        (he : ∀ e' ∈ f.support, e' < e), eval b f < b ^ e)
    {e : Ordinal.{u_1}}
    (hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e'_1 < b)
    (he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e), eval b (single e' x + f) < b ^ e
⊢ eval b f < b ^ e

Tactic:
induction f using Finsupp.induction_on_max generalizing e with
  | zero =>
    rw [eval_zero_right]
    exact opow_pos _ (hb 0)
  | single_add e' x f hf hx IH =>
    have he' : e' ∉ f.support := fun h ↦ (hf _ h).false
    rw [eval_single_add' _ hf]
    apply opow_mul_add_lt_opow _ (IH _ hf)
    · apply he e' _
      simp [hx]
    · apply (hb e').trans_eq'
      rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]
      exact fun h ↦ (hf _ h).false
    · intro a
      by_cases ha : a ∈ f.support
      · apply (hb a).trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        rintro rfl
        contradiction
      · rw [notMem_support_iff.1 ha]
        exact (hb 0).pos

Premises used: LT.lt.pos, Finsupp.single_eq_same, Finsupp.notMem_support_iff, Finsupp.single_eq_of_ne, Finsupp.add_apply, Finsupp.support, zero_add, Finsupp.single_add, Finsupp.induction_on_max, Ordinal.zero, Iff.mp, Ordinal.CNF.eval_zero_right, add_zero, OfNat.ofNat, Ordinal.opow_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
rw : foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)
| o

Tactic:
rw [← CNF.foldr b o]

Premises used: Ordinal.CNF.foldr
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
conv_rhs :
  eval b (coeff b o) =
    foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)
⊢ eval b (coeff b o) = o

Tactic:
conv_rhs => rw [← CNF.foldr b o]

Premises used: Ordinal.CNF.foldr
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
rw :
  Eq (α := Ordinal.{u_1})
    (foldr
      (fun (x : Ordinal.{u_1} × Ordinal.{u_1}) (y : Ordinal.{u_1}) ↦
        HMul.hMul (β := Ordinal.{u_1}) (b ^ x.1)
            ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x.1 : Ordinal.{u_1}) +
          y)
      0 (CNF b o))
    (foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o))
rw₁ : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2) (map Prod.fst (CNF b o))
rw₂ : (map Prod.fst (CNF b o)).Nodup
⊢ eval b (coeff b o) =
    foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)

Tactic:
rw [eval, support_coeff, (toFinset_sort _ _).2, foldr_map]

Premises used: Ordinal.CNF.eval, Iff.mpr, List.toFinset_sort, Ordinal.CNF.support_coeff, List.foldr_map
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
H :
  ∀ a ∈ CNF b o,
    ∀ (b_1 : Ordinal.{u_1}),
      HMul.hMul (β := Ordinal.{u_1}) (b ^ a.1) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a.1 : Ordinal.{u_1}) +
          b_1 =
        b ^ a.1 * a.2 + b_1
⊢ Eq (α := Ordinal.{u_1})
    (foldr
      (fun (x : Ordinal.{u_1} × Ordinal.{u_1}) (y : Ordinal.{u_1}) ↦
        HMul.hMul (β := Ordinal.{u_1}) (b ^ x.1)
            ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x.1 : Ordinal.{u_1}) +
          y)
      0 (CNF b o))
    (foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o))

Tactic:
apply foldr_ext

Premises used: List.foldr_ext
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
x : Ordinal.{u_1}
H H₁ : b ^ a.1 * a.2 + x = b ^ a.1 * a.2 + x
⊢ HMul.hMul (β := Ordinal.{u_1}) (b ^ a.1) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a.1 : Ordinal.{u_1}) + x =
    b ^ a.1 * a.2 + x

Tactic:
rw [coeff_of_mem_CNF ha]

Premises used: Ordinal.CNF.coeff_of_mem_CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2) (map Prod.fst (CNF b o))

Tactic:
(CNF.sortedGT b o).sortedGE.pairwise

Premises used: List.SortedGE.pairwise, Ordinal.CNF.sortedGT, List.SortedGT.sortedGE
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2) (map Prod.fst (CNF b o))

Tactic:
exact (CNF.sortedGT b o).sortedGE.pairwise

Premises used: List.SortedGE.pairwise, Ordinal.CNF.sortedGT, List.SortedGT.sortedGE
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).Nodup

Tactic:
(CNF.sortedGT b o).nodup

Premises used: List.SortedGT.nodup, Ordinal.CNF.sortedGT
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).Nodup

Tactic:
exact (CNF.sortedGT b o).nodup

Premises used: List.SortedGT.nodup, Ordinal.CNF.sortedGT
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
hf : ∀ (e : Ordinal.{u_1}), (0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b
⊢ coeff b (eval b 0) = 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
e' : Ordinal.{u_1}
pos : ∀ (he' : e' ∈ f.support), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
neg : ∀ (he' : e' ∉ f.support), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b

Tactic:
by_cases he' : e' ∈ f.support

Premises used: Finsupp.support
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∈ f.support
pos :
  Eq (α := Ordinal.{u_1}) ((single e x + f : (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

Tactic:
apply (hf e').trans_eq'

Premises used: LT.lt.trans_eq'
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∈ f.support
pos : e' ≠ e
⊢ Eq (α := Ordinal.{u_1}) ((single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})
    ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' : Ordinal.{u_1})

Tactic:
rw [add_apply, single_eq_of_ne, zero_add]

Premises used: Finsupp.single_eq_of_ne, Finsupp.add_apply, zero_add
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∈ f.support
⊢ e' ≠ e

Tactic:
(hf' _ he').ne

Premises used: LT.lt.ne
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∈ f.support
⊢ e' ≠ e

Tactic:
exact (hf' _ he').ne

Premises used: LT.lt.ne
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∉ f.support
neg : 0 < b
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b

Tactic:
rw [notMem_support_iff.1 he']

Premises used: Finsupp.notMem_support_iff, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∉ f.support
⊢ 0 < b

Tactic:
hb.pos

Premises used: LT.lt.pos
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∉ f.support
⊢ 0 < b

Tactic:
exact hb.pos

Premises used: LT.lt.pos
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
⊢ ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b

Tactic:
have IH' (e') : f e' < b := by
      by_cases he' : e' ∈ f.support
      · apply (hf e').trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        exact (hf' _ he').ne
      · rw [notMem_support_iff.1 he']
        exact hb.pos
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
single_add : x < b
single_add₁ : eval b f < b ^ e
⊢ coeff b (eval b (single e x + f)) = single e x + f

Tactic:
rw [eval_single_add' _ hf', coeff_opow_mul_add hb hx, IH IH']

Premises used: Ordinal.CNF.eval_single_add', Ordinal.CNF.coeff_opow_mul_add
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
single_add : (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = x
⊢ x < b

Tactic:
apply (hf e).trans_eq'

Premises used: LT.lt.trans_eq'
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
single_add : e ∉ f.support
⊢ (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = x

Tactic:
rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]

Premises used: Finsupp.single_eq_same, Finsupp.notMem_support_iff, Finsupp.add_apply, Iff.mp, add_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
⊢ e ∉ f.support

Tactic:
fun h ↦ (hf' _ h).false

Premises used: LT.lt.false, Not
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
⊢ e ∉ f.support

Tactic:
exact fun h ↦ (hf' _ h).false

Premises used: LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
⊢ eval b f < b ^ e

Tactic:
eval_lt IH' hf'

Premises used: Ordinal.CNF.eval_lt
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
⊢ eval b f < b ^ e

Tactic:
exact eval_lt IH' hf'

Premises used: Ordinal.CNF.eval_lt
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
hb : 1 < b
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b
zero : ∀ (hf : ∀ (e : Ordinal.{u_1}), (0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b 0) = 0
single_add :
  ∀ (e x : Ordinal.{u_1}) (f : Ordinal.{u_1} →₀ Ordinal.{u_1}) (hf' : ∀ c ∈ f.support, c < e) (hx : x ≠ 0)
    (IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f)
    (hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b),
    coeff b (eval b (single e x + f)) = single e x + f
⊢ coeff b (eval b f) = f

Tactic:
induction f using Finsupp.induction_on_max with
  | zero => simp
  | single_add e x f hf' hx IH =>
    have IH' (e') : f e' < b := by
      by_cases he' : e' ∈ f.support
      · apply (hf e').trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        exact (hf' _ he').ne
      · rw [notMem_support_iff.1 he']
        exact hb.pos
    rw [eval_single_add' _ hf', coeff_opow_mul_add hb hx, IH IH']
    · apply (hf e).trans_eq'
      rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]
      exact fun h ↦ (hf' _ h).false
    · exact eval_lt IH' hf'

Premises used: Finsupp.single_eq_same, Finsupp.notMem_support_iff, Finsupp.add_apply, Finsupp.single_add, Finsupp.induction_on_max, Ordinal.zero, Iff.mp, add_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
⊢ Function.Injective (coeff b)

Tactic:
Function.LeftInverse.injective fun _ ↦ eval_coeff ..

Premises used: Function.LeftInverse.injective, Ordinal.CNF.eval_coeff
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b x y : Ordinal.{u_1}
⊢ coeff b x = coeff b y ↔ x = y

Tactic:
(coeff_injective b).eq_iff

Premises used: Ordinal.CNF.coeff_injective, Function.Injective.eq_iff
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ AddCommute o₁ o₂ ↔
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
⟨fun hcomm ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
refine_1 :
  ∀ (hcomm : AddCommute o₁ o₂),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
refine_2 :
  (∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂) →
    AddCommute o₁ o₂
⊢ AddCommute o₁ o₂ ↔
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
refine ⟨fun hcomm ↦ ?_, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
refine_1 :
  ∀ (o : Ordinal.{u_1})
    (ih :
      ∀ y < o,
        ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
          ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
    {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = o),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
induction h : o₁ + o₂ using WellFoundedLT.induction generalizing o₁ o₂ with | ind o ih

Premises used: WellFoundedLT.induction
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o : Ordinal.{u_1}
ih :
  ∀ y < o,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
h : o₁ + o₂ = o
⊢ ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
subst h
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
refine_1 :
  ∀
    (this :
      ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂)
        (ih :
          ∀ y < o₁ + o₂,
            ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
              ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
        (hle : o₁ ≤ o₂),
        ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
    (hle : ¬o₁ ≤ o₂),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
wlog :
  ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂)
    (ih :
      ∀ y < o₁ + o₂,
        ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
          ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
    (hle : o₁ ≤ o₂),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
wlog hle : o₁ ≤ o₂
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
this :
  ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂)
    (ih :
      ∀ y < o₁ + o₂,
        ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
          ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
    (hle : o₁ ≤ o₂),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : ¬o₁ ≤ o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
grind [hcomm.symm]

Premises used: AddCommute.symm
-- Module: Mathlib.SetTheory.Ordinal.Commute
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
inl :
  ∀ (hcomm : AddCommute 0 o₂)
    (ih :
      ∀ y < 0 + o₂,
        ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
          ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
    (hle : 0 ≤ o₂),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = 0 ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
inr :
  ∀ (h₁ : o₁ ≠ 0),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂

Tactic:
rcases eq_or_ne o₁ 0 with (rfl | h₁)

Premises used: eq_or_ne, OfNat.ofNat, rfl