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}
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 : e' ≠ 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}) =
    (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e'

Tactic:
rw [single_eq_of_ne, zero_add]

Premises used: Finsupp.single_eq_of_ne, zero_add
-- 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}
⊢ e' ≠ e

Tactic:
aesop
-- 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})
⊢ ∀ b ∈ f.support, e ≥ b

Tactic:
fun e' he' ↦ (h e' he').le

Premises used: LT.lt.le
-- 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})
⊢ ∀ b ∈ f.support, e ≥ b

Tactic:
exact fun e' he' ↦ (h e' he').le

Premises used: LT.lt.le
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x : Ordinal.{u_1}
⊢ eval b (single e x) = b ^ e * x

Tactic:
simpa using eval_single_add' b (f := 0)

Premises used: Ordinal.CNF.eval_single_add'
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x : Ordinal.{u_1}
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:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)
⊢ e' ∈ (single e' y + f).support

Tactic:
simp [hy]
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)
single_add₁ : ∀ (he' : e' < e), 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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b 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)

Tactic:
simp only [← add_assoc, ← single_add, eval_single_add' _ hf, mul_add]

Premises used: Ordinal.CNF.eval_single_add', add_assoc, Finsupp.single_add, mul_add
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
single_add : ∀ e'_1 ∈ (single e' y + f).support, e'_1 < e
⊢ eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)

Tactic:
rw [eval_single_add']

Premises used: Ordinal.CNF.eval_single_add'
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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

Tactic:
fun a ha ↦ (h a ha).lt_of_ne ?_

Premises used: LE.le.lt_of_ne
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
single_add : ∀ (a : Ordinal.{u_1}) (ha : a ∈ (single e' y + f).support), a ≠ e
⊢ ∀ e'_1 ∈ (single e' y + f).support, e'_1 < e

Tactic:
refine fun a ha ↦ (h a ha).lt_of_ne ?_

Premises used: LE.le.lt_of_ne
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
apply : a ∈ f.support
⊢ False

Tactic:
apply (hf a _).not_gt he'

Premises used: LT.lt.not_gt
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
⊢ a ∈ f.support

Tactic:
simpa [he'.ne'] using ha

Premises used: LT.lt.ne'
-- 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
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
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)
⊢ eval b (single e x + f) = b ^ e * x + eval b 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

Premises used: Ordinal.CNF.eval_single_add', add_assoc, LE.le.lt_of_ne, Finsupp.single_add, Finsupp.induction_on_max, Ordinal.zero, mul_add, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
h :
  ∀ (e₁ : Ordinal.{u_1}),
    Membership.mem (γ := Finset Ordinal.{u_1}) (support (M := Ordinal.{u_1}) 0) e₁ → ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
⊢ eval b (0 + f₂) = eval b 0 + eval b f₂

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
single_add : ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
single_add₁ : ∀ e' ∈ (f₁ + f₂).support, e' ≤ e₁
⊢ eval b (single e₁ x + f₁ + f₂) = eval b (single e₁ x + f₁) + eval b f₂

Tactic:
rw [add_assoc, eval_single_add, eval_single_add' _ hf₁, IH, add_assoc]

Premises used: Ordinal.CNF.eval_single_add', add_assoc, Ordinal.CNF.eval_single_add
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
⊢ ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
e₂ : Ordinal.{u_1}
he₂ : e₂ ∈ (f₁ + f₂).support
single_add : ∀ (he₂ : e₂ ∈ f₁.support), e₂ ≤ e₁
single_add₁ : ∀ (he₂ : e₂ ∈ f₂.support), e₂ ≤ e₁
⊢ e₂ ≤ e₁

Tactic:
obtain he₂ | he₂ := Finset.mem_union.1 <| support_add he₂

Premises used: Finsupp.support_add, Iff.mp, Finset.mem_union
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
e₂ : Ordinal.{u_1}
he₂_1 : e₂ ∈ (f₁ + f₂).support
he₂ : e₂ ∈ f₁.support
⊢ e₂ ≤ e₁

Tactic:
(hf₁ _ he₂).le

Premises used: LT.lt.le
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
e₂ : Ordinal.{u_1}
he₂_1 : e₂ ∈ (f₁ + f₂).support
he₂ : e₂ ∈ f₁.support
⊢ e₂ ≤ e₁

Tactic:
exact (hf₁ _ he₂).le

Premises used: LT.lt.le
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
e₂ : Ordinal.{u_1}
he₂_1 : e₂ ∈ (f₁ + f₂).support
he₂ : e₂ ∈ f₂.support
apply : e₁ ∈ (single e₁ x + f₁).support
⊢ e₂ ≤ e₁

Tactic:
apply h _ _ _ he₂
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
e₂ : Ordinal.{u_1}
he₂_1 : e₂ ∈ (f₁ + f₂).support
he₂ : e₂ ∈ f₂.support
⊢ e₁ ∈ (single e₁ x + f₁).support

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
f₁ f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e₁ ∈ f₁.support, ∀ 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₂ ∈ f₂.support, e₂ ≤ e₁),
    eval b (0 + f₂) = eval b 0 + eval b f₂
single_add :
  ∀ (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₂
⊢ eval b (f₁ + f₂) = eval b f₁ + eval b f₂

Tactic:
induction f₁ using Finsupp.induction_on_max with
  | zero => simp
  | single_add e₁ x f₁ hf₁ hx IH =>
    rw [add_assoc, eval_single_add, eval_single_add' _ hf₁, IH, add_assoc]
    · simp_all
    · intro e₂ he₂
      obtain he₂ | he₂ := Finset.mem_union.1 <| support_add he₂
      · exact (hf₁ _ he₂).le
      · apply h _ _ _ he₂
        simp_all

Premises used: add_assoc, Finsupp.single_add, Finsupp.induction_on_max, Ordinal.zero, Iff.mp, Finset.mem_union, Ordinal.CNF.eval_single_add
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b 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
zero : 0 < b ^ e
⊢ eval b 0 < b ^ e

Tactic:
rw [eval_zero_right]

Premises used: Ordinal.CNF.eval_zero_right
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b 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
⊢ 0 < b ^ e

Tactic:
opow_pos _ (hb 0)

Premises used: OfNat.ofNat, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b 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
⊢ 0 < b ^ e

Tactic:
exact opow_pos _ (hb 0)

Premises used: OfNat.ofNat, Ordinal.opow_pos
-- 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
⊢ e' ∉ f.support

Tactic:
have he' : e' ∉ f.support := fun h ↦ (hf _ h).false
-- 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
single_add : b ^ e' * x + eval b f < b ^ e
⊢ eval b (single e' x + f) < b ^ e

Tactic:
rw [eval_single_add' _ hf]

Premises used: Ordinal.CNF.eval_single_add'
-- 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
single_add : e' < e
apply : x < b
apply₁ : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
⊢ b ^ e' * x + eval b f < b ^ e

Tactic:
apply opow_mul_add_lt_opow _ (IH _ hf)

Premises used: Ordinal.opow_mul_add_lt_opow
-- 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
apply : e' ∈ (single e' x + f).support
⊢ e' < e

Tactic:
apply he e' _
-- 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
⊢ e' ∈ (single e' x + f).support

Tactic:
simp [hx]
-- 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
apply : (single e' x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' = x
⊢ x < b

Tactic:
apply (hb e').trans_eq'

Premises used: LT.lt.trans_eq'
-- 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' rw : 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 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
⊢ e' ∉ f.support

Tactic:
fun h ↦ (hf _ h).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}
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
⊢ e' ∉ f.support

Tactic:
exact fun h ↦ (hf _ h).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}
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}
pos : ∀ (ha : a ∈ f.support), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b
neg : ∀ (ha : a ∉ f.support), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b

Tactic:
by_cases ha : a ∈ f.support

Premises used: Finsupp.support
-- 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
pos :
  Eq (α := Ordinal.{u_1}) ((single e' x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b

Tactic:
apply (hb a).trans_eq'

Premises used: LT.lt.trans_eq'
-- 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
pos : a ≠ e'
⊢ Eq (α := Ordinal.{u_1}) ((single e' x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : 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 x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
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 a : Ordinal.{u_1}
ha : a ∈ f.support
hf : ∀ c ∈ f.support, c < a
hb : ∀ (e' : Ordinal.{u_1}), (single a x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
he : ∀ e' ∈ (single a x + f).support, e' < e
he' : a ∉ f.support
⊢ False

Tactic:
contradiction
-- 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
neg : 0 < b
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b

Tactic:
rw [notMem_support_iff.1 ha]

Premises used: Finsupp.notMem_support_iff, Iff.mp