awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
⊢ ω ^ e₁.repr * ω ^ e₂.repr = (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ω ^ e₂.repr
have this₁ : ¬e₂.repr = repr 0
Tactic: have := mt repr_inj.1 e0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : ¬e₂ = 0
this_1 : e₁.NF
this_2 : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ^ e₁.repr * ω ^ e₂.repr = (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ω ^ e₂.repr
have neg : ω ∣ ω ^ e₂.repr
Tactic: rw [add_mul_of_isSuccLimit ao (isSuccLimit_opow_left isSuccLimit_omega0 this), mul_assoc,
        mul_omega0_dvd (Nat.cast_pos'.2 n₁.pos) (natCast_lt_omega0 _)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o' : ONote
m : ℕ
h : NF 0
p : split' 0 = (o', m)
⊢ split 0 = (scale 1 o', m)
have fst_eq : 0 = o'
Tactic: injection p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o' : ONote
m : ℕ
h : NF 0
p : split' 0 = (o', m)
fst_eq : 0 = o'
⊢ split 0 = (scale 1 o', m)
have snd_eq : 0 = m
Tactic: injection p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o' : ONote
m : ℕ
h : NF 0
fst_eq : 0 = o'
snd_eq : 0 = m
⊢ split 0 = (scale 1 o', m)
have substs : split 0 = (scale 1 0, 0)
Tactic: substs o' m
Cleared hypotheses: o', m, fst_eq, snd_eq
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
⊢ (e.oadd n a).split = (scale 1 o', m)
have pos : ∀ (e0 : e = 0), (e.oadd n a).split = (scale 1 o', m)
Tactic: by_cases e0 : e = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
pos : ∀ (e0 : e = 0), (e.oadd n a).split = (scale 1 o', m)
⊢ (e.oadd n a).split = (scale 1 o', m)
have neg : ∀ (e0 : ¬e = 0), (e.oadd n a).split = (scale 1 o', m)
Tactic: by_cases e0 : e = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
⊢ (e.oadd n a).split = (scale 1 o', m)
have pos : ∀ (p : 0 = o' ∧ (↑n : ℕ) = m), 0 = scale 1 o' ∧ (↑n : ℕ) = m
Tactic: simp only [split', e0, ↓reduceIte, Prod.mk.injEq, split] at p ⊢
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
⊢ (e.oadd n a).split = (scale 1 o', m)
have neg : ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
Tactic: simp only [split', e0, ↓reduceIte, Prod.mk.injEq, split] at p ⊢
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
have neg : ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
Tactic: revert p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
⊢ ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
have neg : ∀ (a' : ONote) (m' : ℕ) (h' : a.split' = (a', m')) (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
  e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
Tactic: rcases h' : split' a with ⟨a', m'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
have this : e.NF
Tactic: haveI := h.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this : e.NF
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
have this₁ : a.NF
Tactic: haveI := h.snd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
have neg : (e - 1).oadd n a' = o' → m' = m → e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m
Tactic: simp only [split_eq_scale_split' h', and_imp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
⊢ 1 + (e - 1) = e
have refine : (1 + (e - 1)).repr = e.repr
Tactic: refine repr_inj.1 ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
⊢ (1 + (e - 1)).repr = e.repr
have simp : 1 + (e.repr - 1) = e.repr
Tactic: simp only [repr_add, repr_one, Nat.cast_one, repr_sub]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
⊢ 1 + (e.repr - 1) = e.repr
have this₁ : ¬e.repr = repr 0
Tactic: have := mt repr_inj.1 e0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
⊢ (e - 1).oadd n a' = o' → m' = m → e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m
have this₁ : 1 + (e - 1) = e
Tactic: have : 1 + (e - 1) = e := by
        refine repr_inj.1 ?_
        simp only [repr_add, repr_one, Nat.cast_one, repr_sub]
        have := mt repr_inj.1 e0
        exact Ordinal.add_sub_cancel_of_le <| one_le_iff_ne_zero.2 this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
this : 1 + (e - 1) = e
h_1 : (e - 1).oadd n a' = o'
h_2 : m' = m
⊢ e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m
have neg : e.oadd n (scale 1 a') = scale 1 ((e - 1).oadd n a') ∧ m' = m'
Tactic: substs o' m
Cleared hypotheses: o', m, h_1, h_2
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o' : ONote
m : ℕ
h : NF 0
p : split' 0 = (o', m)
⊢ o'.NF ∧ repr 0 = ω * o'.repr + (↑m : Ordinal.{0})
have fst_eq : 0 = o'
Tactic: injection p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o' : ONote
m : ℕ
h : NF 0
p : split' 0 = (o', m)
fst_eq : 0 = o'
⊢ o'.NF ∧ repr 0 = ω * o'.repr + (↑m : Ordinal.{0})
have snd_eq : 0 = m
Tactic: injection p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o' : ONote
m : ℕ
h : NF 0
fst_eq : 0 = o'
snd_eq : 0 = m
⊢ o'.NF ∧ repr 0 = ω * o'.repr + (↑m : Ordinal.{0})
have substs : NF 0 ∧ repr 0 = ω * repr 0 + (↑0 : Ordinal.{0})
Tactic: substs o' m
Cleared hypotheses: o', m, fst_eq, snd_eq
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})
have pos : ∀ (e0 : e = 0), o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})
Tactic: by_cases e0 : e = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
pos : ∀ (e0 : e = 0), o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})
have neg : ∀ (e0 : ¬e = 0), o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})
Tactic: by_cases e0 : e = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})
have pos : ∀ (p : 0 = o' ∧ (↑n : ℕ) = m), o'.NF ∧ (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
Tactic: simp only [split', e0, ↓reduceIte, Prod.mk.injEq, repr, repr_zero, opow_zero, one_mul] at p ⊢
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})
have p₁ : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
Tactic: simp only [split', e0, ↓reduceIte, Prod.mk.injEq, repr, repr_zero, opow_zero, one_mul] at p ⊢
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : e = 0
p : 0 = o' ∧ (↑n : ℕ) = m
⊢ o'.NF ∧ (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
have pos : NF 0 ∧ (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * repr 0 + (↑(↑n : ℕ) : Ordinal.{0})
Tactic: rcases p with ⟨rfl, rfl⟩
Cleared hypotheses: o', m, p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
have neg : ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m),
  o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
Tactic: revert p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
⊢ ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
have neg : ∀ (a' : ONote) (m' : ℕ) (h' : a.split' = (a', m')) (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
  o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
Tactic: rcases h' : split' a with ⟨a', m'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
have this : e.NF
Tactic: haveI := h.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this : e.NF
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
have this₁ : a.NF
Tactic: haveI := h.snd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
have IH₁ : a'.NF
Tactic: obtain ⟨IH₁, IH₂⟩ := nf_repr_split' h'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
IH₁ : a'.NF
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
have IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
Tactic: obtain ⟨IH₁, IH₂⟩ := nf_repr_split' h'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
have neg : (e - 1).oadd n a' = o' →
  m' = m →
    o'.NF ∧
      ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) = ω * o'.repr + (↑m : Ordinal.{0})
Tactic: simp only [IH₂, and_imp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
h_1 : (e - 1).oadd n a' = o'
h_2 : m' = m
⊢ o'.NF ∧
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) = ω * o'.repr + (↑m : Ordinal.{0})
have neg : ((e - 1).oadd n a').NF ∧
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
    ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
Tactic: substs o' m
Cleared hypotheses: o', m, h_1, h_2
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
⊢ ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
have this₁ : ¬e.repr = repr 0
Tactic: have := mt repr_inj.1 e0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ¬e.repr = repr 0
⊢ ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
have rw : ω ^ e.repr = ω ^ (1 + (e.repr - 1))
Tactic: rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ¬e.repr = repr 0
rw : ω ^ e.repr = ω ^ (1 + (e.repr - 1))
⊢ ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
have rw₁ : ω ^ e.repr = ω ^ e.repr
Tactic: rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
⊢ ((e - 1).oadd n a').NF ∧
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
      ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
have this₁ : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
Tactic: have : (ω : Ordinal.{0}) ^ repr e = ω ^ (1 : Ordinal.{0}) * ω ^ (repr e - 1) := by
        have := mt repr_inj.1 e0
        rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
⊢ ((e - 1).oadd n a').NF ∧
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
      ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
have neg : a'.NFBelow (e - 1).repr
Tactic: refine ⟨NF.oadd (by infer_instance) _ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
neg : a'.NFBelow (e - 1).repr
⊢ ((e - 1).oadd n a').NF ∧
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
      ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
have neg₁ : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
  ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
Tactic: refine ⟨NF.oadd (by infer_instance) _ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
⊢ a'.NFBelow (e - 1).repr
have neg : ∀ (this : ω ^ e.repr = ω * ω ^ (e.repr - 1)), a'.NFBelow (e.repr - 1)
Tactic: simp only [opow_one, repr_sub, repr_one, Nat.cast_one] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
⊢ a'.NFBelow (e.repr - 1)
have neg : ω * a'.repr + (↑m' : Ordinal.{0}) < ω * ω ^ (e.repr - 1)
Tactic: refine IH₁.below_of_lt' <| (mul_lt_mul_iff_right₀ omega0_pos).1 <|
          (le_self_add (α := Ordinal) (b := m')).trans_lt ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
⊢ ω * a'.repr + (↑m' : Ordinal.{0}) < ω * ω ^ (e.repr - 1)
have neg : a.repr < ω ^ e.repr
Tactic: rw [← this, ← IH₂]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
    ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
have neg : HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1) * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
  ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
have this : a.NF
Tactic: haveI := h.snd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
have pos : ∀ (e0 : e = 0), (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
Tactic: by_cases e0 : e = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
pos : ∀ (e0 : e = 0), (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
have neg : ∀ (e0 : ¬e = 0), (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
Tactic: by_cases e0 : e = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
have pos : (x + e).oadd n (x.oadd 1 0 * a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
Tactic: simp_rw [scale_eq_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
x : ONote
inst : x.NF
o : ONote
inst_1 : o.NF
⊢ (x.scale o).NF
have rw : (x.oadd 1 0 * o).NF
Tactic: rw [scale_eq_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
⊢ o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})
have rcases : ∀ (a : ONote) (n : ℕ) (e : o.split' = (a, n)), o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})
Tactic: rcases e : split' o with ⟨a, n⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})
have s₁ : a.NF
Tactic: obtain ⟨s₁, s₂⟩ := nf_repr_split' e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
⊢ o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})
have s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
Tactic: obtain ⟨s₁, s₂⟩ := nf_repr_split' e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
⊢ o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})
have h₁ : (scale 1 a, n) = (o', m)
Tactic: rw [split_eq_scale_split' e] at h
Cleared hypotheses: h, e, s₁, s₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
⊢ o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})
have fst_eq : scale 1 a = o'
Tactic: injection h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
fst_eq : scale 1 a = o'
⊢ o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})
have snd_eq : n = m
Tactic: injection h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
fst_eq : scale 1 a = o'
snd_eq : n = m
⊢ o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})
have substs : ∀ (e : o.split' = (a, m)) (s₂ : o.repr = ω * a.repr + (↑m : Ordinal.{0})),
  (scale 1 a).NF ∧ o.repr = (scale 1 a).repr + (↑m : Ordinal.{0})
Tactic: substs o' n
Cleared hypotheses: o', n, e, s₂, fst_eq, snd_eq
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
m : ℕ
inst : o.NF
a : ONote
s₁ : a.NF
e : o.split' = (a, m)
s₂ : o.repr = ω * a.repr + (↑m : Ordinal.{0})
⊢ (scale 1 a).NF ∧ o.repr = (scale 1 a).repr + (↑m : Ordinal.{0})
have simp : (scale 1 a).NF
Tactic: simp only [repr_scale, repr_one, Nat.cast_one, opow_one, ← s₂, and_true]