awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
⊢ e.oadd n a + o = e.addAux n (a + o)

Tactic:
rfl

Premises used: ONote.add, ONote.addAux, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (a + o).NFBelow b

Tactic:
have h' := add_nfBelow (h₁.snd.mono <| le_of_lt h₁.lt) h₂
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
simp : (e.addAux n (a + o)).NFBelow b
⊢ (e.oadd n a + o).NFBelow b

Tactic:
simp only [oadd_add]

Premises used: ONote.oadd_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
revert : ∀ (h' : (a + o).NFBelow b), (e.addAux n (a + o)).NFBelow b
⊢ (e.addAux n (a + o)).NFBelow b

Tactic:
revert h'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
zero : ∀ (h' : ONote.zero.NFBelow b), (e.addAux n ONote.zero).NFBelow b
oadd : ∀ (e' : ONote) (n' : ℕ+) (a' : ONote) (h' : (e'.oadd n' a').NFBelow b), (e.addAux n (e'.oadd n' a')).NFBelow b
⊢ ∀ (h' : (a + o).NFBelow b), (e.addAux n (a + o)).NFBelow b

Tactic:
obtain - | ⟨e', n', a'⟩ := a + o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : zero.NFBelow b
⊢ (e.addAux n zero).NFBelow b

Tactic:
NFBelow.oadd h₁.fst NFBelow.zero h₁.lt

Premises used: ONote.NFBelow.oadd, ONote.NFBelow.lt, ONote.NFBelow.zero, ONote.addAux, ONote.NFBelow.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : zero.NFBelow b
⊢ (e.addAux n zero).NFBelow b

Tactic:
exact NFBelow.oadd h₁.fst NFBelow.zero h₁.lt

Premises used: ONote.NFBelow.oadd, ONote.NFBelow.lt, ONote.NFBelow.zero, ONote.NFBelow.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
⊢ (e.cmp e').Compares e e'

Tactic:
have : ((e.cmp e').Compares e e') := @cmp_compares _ _ h₁.fst h'.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
oadd : ∀ (h : e.cmp e' = Ordering.lt), (e.addAux n (e'.oadd n' a')).NFBelow b
oadd₁ : ∀ (h : e.cmp e' = Ordering.eq), (e.addAux n (e'.oadd n' a')).NFBelow b
oadd₂ : ∀ (h : e.cmp e' = Ordering.gt), (e.addAux n (e'.oadd n' a')).NFBelow b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
cases h : cmp e e'

Premises used: ONote.cmp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
oadd :
  NFBelow
    (match (motive := Ordering → ONote) e.cmp e' with
    | Ordering.lt => e'.oadd n' a'
    | Ordering.eq => e.oadd (n + n') a'
    | Ordering.gt => e.oadd n (e'.oadd n' a'))
    b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
dsimp [addAux]

Premises used: ONote.addAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
oadd :
  NFBelow
    (match (motive := Ordering → ONote) e.cmp e' with
    | Ordering.lt => e'.oadd n' a'
    | Ordering.eq => e.oadd (n + n') a'
    | Ordering.gt => e.oadd n (e'.oadd n' a'))
    b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
dsimp [addAux]

Premises used: ONote.addAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
oadd :
  NFBelow
    (match (motive := Ordering → ONote) e.cmp e' with
    | Ordering.lt => e'.oadd n' a'
    | Ordering.eq => e.oadd (n + n') a'
    | Ordering.gt => e.oadd n (e'.oadd n' a'))
    b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
dsimp [addAux]

Premises used: ONote.addAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
oadd : (e'.oadd n' a').NFBelow b
⊢ NFBelow
    (match (motive := Ordering → ONote) e.cmp e' with
    | Ordering.lt => e'.oadd n' a'
    | Ordering.eq => e.oadd (n + n') a'
    | Ordering.gt => e.oadd n (e'.oadd n' a'))
    b

Tactic:
simp only [h]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
oadd : (e.oadd (n + n') a').NFBelow b
⊢ NFBelow
    (match (motive := Ordering → ONote) e.cmp e' with
    | Ordering.lt => e'.oadd n' a'
    | Ordering.eq => e.oadd (n + n') a'
    | Ordering.gt => e.oadd n (e'.oadd n' a'))
    b

Tactic:
simp only [h]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
oadd : (e.oadd n (e'.oadd n' a')).NFBelow b
⊢ NFBelow
    (match (motive := Ordering → ONote) e.cmp e' with
    | Ordering.lt => e'.oadd n' a'
    | Ordering.eq => e.oadd (n + n') a'
    | Ordering.gt => e.oadd n (e'.oadd n' a'))
    b

Tactic:
simp only [h]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (e'.oadd n' a').NFBelow b

Tactic:
h'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (e'.oadd n' a').NFBelow b

Tactic:
exact h'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ Ordering.eq.Compares e e'

Tactic:
simp only [h] at this
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.eq
this : Ordering.eq.Compares e e'
⊢ (e.oadd n' a').NFBelow b

Tactic:
subst e'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.eq
this : Ordering.eq.Compares e e'
h'₁ : (e.oadd n' a').NFBelow b
⊢ e.cmp e = Ordering.eq

Tactic:
subst e'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
n' : ℕ+
a' : ONote
h' : (e.oadd n' a').NFBelow b
h : e.cmp e = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

Tactic:
NFBelow.oadd h'.fst h'.snd h'.lt

Premises used: ONote.NFBelow.oadd, ONote.NFBelow.lt, ONote.NFBelow.snd, ONote.NFBelow.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
n' : ℕ+
a' : ONote
h' : (e.oadd n' a').NFBelow b
h : e.cmp e = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

Tactic:
exact NFBelow.oadd h'.fst h'.snd h'.lt

Premises used: ONote.NFBelow.oadd, ONote.NFBelow.lt, ONote.NFBelow.snd, ONote.NFBelow.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ Ordering.gt.Compares e e'

Tactic:
simp only [h] at this
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.gt
this : Ordering.gt.Compares e e'
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b

Tactic:
NFBelow.oadd h₁.fst (NF.below_of_lt this ⟨⟨_, h'⟩⟩) h₁.lt

Premises used: ONote.NFBelow.oadd, ONote.NFBelow.lt, ONote.NF.below_of_lt, Exists.intro, ONote.NFBelow.fst, ONote.NF.mk
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.gt
this : Ordering.gt.Compares e e'
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b

Tactic:
exact NFBelow.oadd h₁.fst (NF.below_of_lt this ⟨⟨_, h'⟩⟩) h₁.lt

Premises used: ONote.NFBelow.oadd, ONote.NFBelow.lt, ONote.NF.below_of_lt, Exists.intro, ONote.NFBelow.fst, ONote.NF.mk
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
h : NF 0
h_1 : o.NF
⊢ (0 + o).repr = repr 0 + o.repr

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
⊢ a.NF

Tactic:
haveI := h₁.snd
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
⊢ (a + o).repr = a.repr + o.repr

Tactic:
have h' := repr_add a o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a + o).repr = a.repr + o.repr
⊢ (a.add o).repr = a.repr + o.repr

Tactic:
conv_lhs at h' => simp [HAdd.hAdd, Add.add]

Premises used: Add.add, HAdd.hAdd
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
⊢ (a + o).NF

Tactic:
have nf := ONote.add_nf a o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a + o).NF
⊢ (a.add o).NF

Tactic:
conv at nf => simp [HAdd.hAdd, Add.add]

Premises used: Add.add, HAdd.hAdd
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a.add o).NF
zero : ∀ (h : a.add o = ONote.zero), ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
oadd :
  ∀ (e' : ONote) (n' : ℕ+) (a' : ONote) (h : a.add o = e'.oadd n' a'),
    ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr

Tactic:
rcases h : add a o with - | ⟨e', n', a'⟩

Premises used: ONote.add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a.add o).NF
h : a.add o = zero
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr

Tactic:
simp only [add, addAux, h'.symm, h, add_assoc, repr] at nf h₁ ⊢

Premises used: ONote.add, add_assoc, ONote.addAux, ONote.repr, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a.add o).NF
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
oadd :
  ∀ (nf : (e'.oadd n' a').NF),
    repr
        (match (motive := Ordering → ONote) e.cmp e' with
        | Ordering.lt => e'.oadd n' a'
        | Ordering.eq => e.oadd (n + n') a'
        | Ordering.gt => e.oadd n (e'.oadd n' a')) =
      ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr

Tactic:
simp only [add, addAux, h'.symm, h, add_assoc, repr] at nf h₁ ⊢

Premises used: ONote.add, add_assoc, ONote.addAux, ONote.repr, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
⊢ e.NF

Tactic:
have := h₁.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this : e.NF
⊢ e'.NF

Tactic:
haveI := nf.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
⊢ (e.cmp e').Compares e e'

Tactic:
have ee := cmp_compares e e'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
oadd :
  ∀ (he : e.cmp e' = Ordering.lt),
    repr
        (match (motive := Ordering → ONote) Ordering.lt with
        | Ordering.lt => e'.oadd n' a'
        | Ordering.eq => e.oadd (n + n') a'
        | Ordering.gt => e.oadd n (e'.oadd n' a')) =
      ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
oadd₁ :
  ∀ (he : e.cmp e' = Ordering.eq),
    repr
        (match (motive := Ordering → ONote) Ordering.eq with
        | Ordering.lt => e'.oadd n' a'
        | Ordering.eq => e.oadd (n + n') a'
        | Ordering.gt => e.oadd n (e'.oadd n' a')) =
      ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
oadd₂ :
  ∀ (he : e.cmp e' = Ordering.gt),
    repr
        (match (motive := Ordering → ONote) Ordering.gt with
        | Ordering.lt => e'.oadd n' a'
        | Ordering.eq => e.oadd (n + n') a'
        | Ordering.gt => e.oadd n (e'.oadd n' a')) =
      ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
⊢ repr
      (match (motive := Ordering → ONote) e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)

Tactic:
cases he : cmp e e'

Premises used: ONote.cmp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.lt
⊢ e < e'

Tactic:
simp only [he, Ordering.compares_gt, Ordering.compares_lt,
        Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢

Premises used: Ordering.compares_gt, PNat.add_coe, Nat.cast_add, Ordering.compares_eq, ONote.repr, gt_iff_lt, Ordering.compares_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.eq
oadd :
  ∀ (ee : e = e'),
    ω ^ e.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
      ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
⊢ repr
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)

Tactic:
simp only [he, Ordering.compares_gt, Ordering.compares_lt,
        Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢

Premises used: Ordering.compares_gt, PNat.add_coe, Nat.cast_add, Ordering.compares_eq, ONote.repr, gt_iff_lt, Ordering.compares_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.gt
⊢ repr
      (match (motive := Ordering → ONote) Ordering.gt with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)

Tactic:
simp only [he, Ordering.compares_gt, Ordering.compares_lt,
        Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢

Premises used: Ordering.compares_gt, PNat.add_coe, Nat.cast_add, Ordering.compares_eq, ONote.repr, gt_iff_lt, Ordering.compares_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
oadd : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ e'.repr
oadd₁ : ω ^ e'.repr ≤ ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0})
⊢ ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)

Tactic:
rw [← add_assoc, @add_of_omega0_opow_le _ (repr e') (ω ^ repr e' * (n' : ℕ))]

Premises used: add_assoc, Ordinal.add_of_omega0_opow_le
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ (e.oadd n a).repr < ω ^ e'.repr

Tactic:
have := (h₁.below_of_lt ee).repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this : (e.oadd n a).repr < ω ^ e'.repr
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr <
    HPow.hPow (β := Ordinal.{0}) ω
      (match (motive := ONote → Ordinal.{0}) e' with
        | zero => 0
        | e.oadd n a => ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr :
        Ordinal.{0})

Tactic:
unfold repr at this

Premises used: ONote.repr
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this :
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr <
    HPow.hPow (β := Ordinal.{0}) ω
      (match (motive := ONote → Ordinal.{0}) e' with
        | zero => 0
        | e.oadd n a => ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr :
        Ordinal.{0})
oadd : ∀ (he' : e' = zero), ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ zero.repr
oadd₁ :
  ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote) (he' : e' = a.oadd a_1 a_2),
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ (a.oadd a_1 a_2).repr
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ e'.repr

Tactic:
cases he' : e'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this :
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr <
    HPow.hPow (β := Ordinal.{0}) ω
      (match (motive := ONote → Ordinal.{0}) e' with
        | zero => 0
        | e.oadd n a => ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr :
        Ordinal.{0})
he' : e' = zero
oadd : ∀ (this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < 1), ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < 1
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ zero.repr

Tactic:
simp only [he', zero_def, opow_zero, repr, gt_iff_lt] at this ⊢

Premises used: ONote.repr, Ordinal.opow_zero, gt_iff_lt, ONote.zero_def
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this :
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr <
    HPow.hPow (β := Ordinal.{0}) ω
      (match (motive := ONote → Ordinal.{0}) e' with
        | zero => 0
        | e.oadd n a => ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr :
        Ordinal.{0})
a_1 : ONote
a_2 : ℕ+
a_3 : ONote
he' : e' = a_1.oadd a_2 a_3
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ (ω ^ a_1.repr * (↑(↑a_2 : ℕ) : Ordinal.{0}) + a_3.repr)

Tactic:
simp only [he', zero_def, opow_zero, repr, gt_iff_lt] at this ⊢

Premises used: ONote.repr, Ordinal.opow_zero, gt_iff_lt, ONote.zero_def
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
he' : e' = zero
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < 1
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < 1

Tactic:
lt_of_le_of_lt le_self_add this

Premises used: lt_of_le_of_lt, le_self_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
he' : e' = zero
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < 1
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < 1

Tactic:
exact lt_of_le_of_lt le_self_add this

Premises used: lt_of_le_of_lt, le_self_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this_3 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
a_1 : ONote
a_2 : ℕ+
a_3 : ONote
he' : e' = a_1.oadd a_2 a_3
this : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ (ω ^ a_1.repr * (↑(↑a_2 : ℕ) : Ordinal.{0}) + a_3.repr)
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) < ω ^ (ω ^ a_1.repr * (↑(↑a_2 : ℕ) : Ordinal.{0}) + a_3.repr)

Tactic:
lt_of_le_of_lt le_self_add this

Premises used: lt_of_le_of_lt, le_self_add