awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
single_add : ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
⊢ eval b (single e₁ x + f₁ + f₂) = eval b (single e₁ x + f₁) + eval b f₂
have single_add₁ : ∀ e' ∈ (f₁ + f₂).support, e' ≤ e₁
Tactic: rw [add_assoc, eval_single_add, eval_single_add' _ hf₁, IH, add_assoc]
-- 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
e₂ : Ordinal.{u_1}
he₂ : e₂ ∈ (f₁ + f₂).support
⊢ e₂ ≤ e₁
have single_add : ∀ (he₂ : e₂ ∈ f₁.support), e₂ ≤ e₁
Tactic: obtain he₂ | he₂ := Finset.mem_union.1 <| support_add he₂
-- 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
e₂ : Ordinal.{u_1}
he₂ : e₂ ∈ (f₁ + f₂).support
single_add : ∀ (he₂ : e₂ ∈ f₁.support), e₂ ≤ e₁
⊢ e₂ ≤ e₁
have single_add₁ : ∀ (he₂ : e₂ ∈ f₂.support), e₂ ≤ e₁
Tactic: obtain he₂ | he₂ := Finset.mem_union.1 <| support_add he₂
-- 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
e₂ : Ordinal.{u_1}
he₂_1 : e₂ ∈ (f₁ + f₂).support
he₂ : e₂ ∈ f₂.support
⊢ e₂ ≤ e₁
have apply : e₁ ∈ (single e₁ x + f₁).support
Tactic: apply h _ _ _ he₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
f₁ f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
⊢ eval b (f₁ + f₂) = eval b f₁ + eval b f₂
have 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₂
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
Cleared hypotheses: f₁, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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₂
⊢ eval b (f₁ + f₂) = eval b f₁ + eval b f₂
have 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₂
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
Cleared hypotheses: f₁, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ eval b 0 < b ^ e
have zero : 0 < b ^ e
Tactic: rw [eval_zero_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (hypothesis)
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
⊢ eval b (single e' x + f) < b ^ e
have he' : e' ∉ f.support
Tactic: have he' : e' ∉ f.support := fun h ↦ (hf _ h).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}
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
⊢ eval b (single e' x + f) < b ^ e
have single_add : b ^ e' * x + eval b f < b ^ e
Tactic: rw [eval_single_add' _ hf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ b ^ e' * x + eval b f < b ^ e
have single_add : e' < e
Tactic: apply opow_mul_add_lt_opow _ (IH _ hf)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ b ^ e' * x + eval b f < b ^ e
have apply : x < b
Tactic: apply opow_mul_add_lt_opow _ (IH _ hf)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ b ^ e' * x + eval b f < b ^ e
have apply₁ : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
Tactic: apply opow_mul_add_lt_opow _ (IH _ hf)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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' < e
have apply : e' ∈ (single e' x + f).support
Tactic: apply he e' _
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ x < b
have apply : (single e' x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' = x
Tactic: apply (hb e').trans_eq'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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}
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b
have pos : ∀ (ha : a ∈ f.support), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b
Tactic: by_cases ha : a ∈ f.support
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b
have neg : ∀ (ha : a ∉ f.support), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b
Tactic: by_cases ha : a ∈ f.support
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b
have 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})
Tactic: apply (hb a).trans_eq'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ 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})
have pos : a ≠ e'
Tactic: rw [add_apply, single_eq_of_ne, zero_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a < b
have neg : 0 < b
Tactic: rw [notMem_support_iff.1 ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ eval b f < b ^ e
have 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
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
Cleared hypotheses: e, f, hb, he
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ eval b f < b ^ e
have 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
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
Cleared hypotheses: e, f, hb, he
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
| o
have rw : 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 [← CNF.foldr b o]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
⊢ eval b (coeff b o) = o
have 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)
Tactic: conv_rhs => rw [← CNF.foldr b o]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
⊢ 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)
have 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))
Tactic: rw [eval, support_coeff, (toFinset_sort _ _).2, foldr_map]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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))
⊢ 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)
have rw₁ : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ≥ x2) (map Prod.fst (CNF b o))
Tactic: rw [eval, support_coeff, (toFinset_sort _ _).2, foldr_map]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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))
⊢ 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)
have rw₂ : (map Prod.fst (CNF b o)).Nodup
Tactic: rw [eval, support_coeff, (toFinset_sort _ _).2, foldr_map]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_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))
have 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
Tactic: apply foldr_ext
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
x : 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}) + x =
    b ^ a.1 * a.2 + x
have H : b ^ a.1 * a.2 + x = b ^ a.1 * a.2 + x
Tactic: rw [coeff_of_mem_CNF ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
have pos : ∀ (he' : e' ∈ f.support), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
Tactic: by_cases he' : e' ∈ f.support
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
have neg : ∀ (he' : e' ∉ f.support), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
Tactic: by_cases he' : e' ∈ f.support
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
have 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})
Tactic: apply (hf e').trans_eq'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ 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})
have pos : e' ≠ e
Tactic: rw [add_apply, single_eq_of_ne, zero_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
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
⊢ (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
have neg : 0 < b
Tactic: rw [notMem_support_iff.1 he']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (hypothesis)
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
⊢ coeff b (eval b (single e x + f)) = single e x + f
have IH' : ∀ (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