awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
lt :
  repr
      (match (motive := Ordering → ONote) Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁) =
    0
lt₁ : (e₁.oadd n₁ a₁).repr ≤ (e₂.oadd n₂ a₂).repr
⊢ repr
      (match (motive := Ordering → ONote) Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁) =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
rw [Ordinal.sub_eq_zero_iff_le.2]

Premises used: Iff.mpr, Ordinal.sub_eq_zero_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ repr
      (match (motive := Ordering → ONote) Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁) =
    0

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (e₁.oadd n₁ a₁).repr ≤ (e₂.oadd n₂ a₂).repr

Tactic:
le_of_lt (oadd_lt_oadd_1 h₁ ee)

Premises used: le_of_lt, ONote.oadd_lt_oadd_1
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (e₁.oadd n₁ a₁).repr ≤ (e₂.oadd n₂ a₂).repr

Tactic:
exact le_of_lt (oadd_lt_oadd_1 h₁ ee)

Premises used: le_of_lt, ONote.oadd_lt_oadd_1
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.eq
ee : Ordering.eq.Compares e₁ e₂
⊢ e₁ = e₂

Tactic:
change e₁ = e₂ at ee
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.eq
ee : e₁ = e₂
eq :
  ∀ (h₂ : (e₁.oadd n₂ a₂).NF) (h : e₁.cmp e₁ = Ordering.eq),
    repr
        (match (motive := Ordering → ONote) Ordering.eq with
        | Ordering.lt => 0
        | Ordering.gt => e₁.oadd n₁ a₁
        | Ordering.eq =>
          match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
          | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
          | k.succ => e₁.oadd k.succPNat a₁) =
      (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
⊢ repr
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁) =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
subst e₂
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
eq :
  repr
      (match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁) =
    (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
⊢ repr
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁) =
    (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
dsimp only
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
eq :
  ∀ (mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = 0),
    repr
        (match (motive := ℕ → ONote) 0 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁) =
      (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
eq₁ :
  ∀ (n : ℕ) (mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1),
    repr
        (match (motive := ℕ → ONote) n + 1 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁) =
      (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
⊢ repr
      (match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁) =
    (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
cases mn : (n₁ : ℕ) - n₂

Premises used: PNat.val
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = 0
pos : ∀ (en : n₁ = n₂), (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
neg : ∀ (en : ¬n₁ = n₂), (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
by_cases en : n₁ = n₂
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = 0
en : n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
simpa [en]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = 0
en : ¬n₁ = n₂
neg : repr 0 = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
simp only [en, ite_false]

Premises used: ite_false
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = 0
en : ¬n₁ = n₂
⊢ repr 0 = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
(Ordinal.sub_eq_zero_iff_le.2 <|
                le_of_lt <|
                  oadd_lt_oadd_2 h₁ <|
                    lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt PNat.eq en)).symm

Premises used: Iff.mpr, Ordinal.sub_eq_zero_iff_le, le_of_lt, mt, tsub_eq_zero_iff_le, ONote.repr, Iff.mp, ONote.oadd_lt_oadd_2, Eq.symm, PNat.eq, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = 0
en : ¬n₁ = n₂
⊢ repr 0 = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
exact
            (Ordinal.sub_eq_zero_iff_le.2 <|
                le_of_lt <|
                  oadd_lt_oadd_2 h₁ <|
                    lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt PNat.eq en)).symm

Premises used: Iff.mpr, Ordinal.sub_eq_zero_iff_le, le_of_lt, mt, tsub_eq_zero_iff_le, Iff.mp, ONote.oadd_lt_oadd_2, Eq.symm, PNat.eq, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1
eq :
  ω ^ e₁.repr * (↑(succ n) : Ordinal.{0}) + a₁.repr =
    ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr - (ω ^ e₁.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)
⊢ (e₁.oadd n.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
simp only [Nat.succPNat, Nat.succ_eq_add_one, repr, PNat.mk_coe, ← succ_eq_add_one]

Premises used: Nat.succ_eq_add_one, Order.succ_eq_add_one, ONote.repr, Nat.succPNat, PNat.mk_coe
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1
eq : ω ^ e₁.repr * (↑(succ n) : Ordinal.{0}) + a₁.repr = ω ^ e₁.repr * (↑(n + 1) : Ordinal.{0}) + a₁.repr - a₂.repr
⊢ ω ^ e₁.repr * (↑(succ n) : Ordinal.{0}) + a₁.repr =
    ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr - (ω ^ e₁.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)

Tactic:
rw [(tsub_eq_iff_eq_add_of_le <| le_of_lt <| Nat.lt_of_sub_eq_succ mn).1 mn, add_comm,
          Nat.cast_add, mul_add, add_assoc, add_sub_add_cancel]

Premises used: add_assoc, le_of_lt, add_comm, tsub_eq_iff_eq_add_of_le, Nat.cast_add, Iff.mp, mul_add, Ordinal.add_sub_add_cancel, Nat.lt_of_sub_eq_succ
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1
⊢ ω ^ e₁.repr * (↑(succ n) : Ordinal.{0}) + a₁.repr = ω ^ e₁.repr * (↑(n + 1) : Ordinal.{0}) + a₁.repr - a₂.repr

Tactic:
(Ordinal.sub_eq_of_add_eq <|
              add_of_omega0_opow_le h₂.snd'.repr_lt <| le_trans ?_ le_self_add).symm

Premises used: Order.succ, Ordinal.add_of_omega0_opow_le, Ordinal.sub_eq_of_add_eq, Eq.symm, le_self_add, ONote.NF.snd', ONote.NFBelow.repr_lt, le_trans
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1
eq : ω ^ e₁.repr ≤ ω ^ e₁.repr * (↑(succ n) : Ordinal.{0})
⊢ ω ^ e₁.repr * (↑(succ n) : Ordinal.{0}) + a₁.repr = ω ^ e₁.repr * (↑(n + 1) : Ordinal.{0}) + a₁.repr - a₂.repr

Tactic:
refine
          (Ordinal.sub_eq_of_add_eq <|
              add_of_omega0_opow_le h₂.snd'.repr_lt <| le_trans ?_ le_self_add).symm

Premises used: Ordinal.add_of_omega0_opow_le, Ordinal.sub_eq_of_add_eq, Eq.symm, le_self_add, ONote.NF.snd', ONote.NFBelow.repr_lt, le_trans
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1
⊢ ω ^ e₁.repr ≤ ω ^ e₁.repr * (↑(succ n) : Ordinal.{0})

Tactic:
Ordinal.le_mul_left _ (Nat.cast_lt.2 <| Nat.succ_pos _)

Premises used: Iff.mpr, Nat.succ_pos, Ordinal.le_mul_left, Nat.cast_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1
⊢ ω ^ e₁.repr ≤ ω ^ e₁.repr * (↑(succ n) : Ordinal.{0})

Tactic:
exact Ordinal.le_mul_left _ (Nat.cast_lt.2 <| Nat.succ_pos _)

Premises used: Iff.mpr, Nat.succ_pos, Ordinal.le_mul_left, Nat.cast_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.gt
ee : Ordering.gt.Compares e₁ e₂
⊢ repr
      (match (motive := Ordering → ONote) Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁) =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
(Ordinal.sub_eq_of_add_eq <|
            add_of_omega0_opow_le (h₂.below_of_lt ee).repr_lt <| omega0_le_oadd _ _ _).symm

Premises used: Ordinal.add_of_omega0_opow_le, ONote.omega0_le_oadd, ONote.NF.below_of_lt, Ordinal.sub_eq_of_add_eq, Eq.symm, ONote.NFBelow.repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.gt
ee : Ordering.gt.Compares e₁ e₂
⊢ repr
      (match (motive := Ordering → ONote) Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ) - (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁) =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
exact
        (Ordinal.sub_eq_of_add_eq <|
            add_of_omega0_opow_le (h₂.below_of_lt ee).repr_lt <| omega0_le_oadd _ _ _).symm

Premises used: Ordinal.add_of_omega0_opow_le, ONote.omega0_le_oadd, ONote.NF.below_of_lt, Ordinal.sub_eq_of_add_eq, Eq.symm, ONote.NFBelow.repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
zero : 0 * ONote.zero = 0
oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote), 0 * a.oadd a_1 a_2 = 0
⊢ 0 * o = 0

Tactic:
cases o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ 0 * zero = 0

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
a_1 : ℕ+
a_2 : ONote
⊢ 0 * a.oadd a_1 a_2 = 0

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
zero : ONote.zero * 0 = 0
oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote), a.oadd a_1 a_2 * 0 = 0
⊢ o * 0 = 0

Tactic:
cases o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ zero * 0 = 0

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
a_1 : ℕ+
a_2 : ONote
⊢ a.oadd a_1 a_2 * 0 = 0

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂ = if e₂ = 0 then e₁.oadd (n₁ * n₂) a₁ else (e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)

Tactic:
rfl

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

Tactic:
have IH := oadd_mul_nfBelow h₁ h₂.snd
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
pos : ∀ (e0 : e₂ = 0), (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
neg : ∀ (e0 : ¬e₂ = 0), (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

Tactic:
by_cases e0 : e₂ = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
pos : (e₁.oadd (n₁ * n₂) a₁).NFBelow (e₁.repr + b₂)
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

Tactic:
simp only [e0, oadd_mul, ↓reduceIte]

Premises used: reduceIte, ONote.oadd_mul
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
neg : ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

Tactic:
simp only [e0, oadd_mul, ↓reduceIte]

Premises used: reduceIte, ONote.oadd_mul
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
pos : e₁.repr < e₁.repr + b₂
⊢ (e₁.oadd (n₁ * n₂) a₁).NFBelow (e₁.repr + b₂)

Tactic:
apply NFBelow.oadd h₁.fst h₁.snd

Premises used: ONote.NFBelow.oadd, ONote.NFBelow.snd, ONote.NFBelow.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ e₁.repr < e₁.repr + b₂

Tactic:
simpa using (add_lt_add_iff_left (repr e₁)).2 h₂.lt.pos

Premises used: Iff.mpr, LT.lt.pos, ONote.NFBelow.lt, ONote.repr, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
⊢ e₁.NF

Tactic:
haveI := h₁.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this : e₁.NF
⊢ e₂.NF

Tactic:
haveI := h₂.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
neg : (e₁ + e₂).NF
neg₁ : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁ + e₂).repr
neg₂ : (e₁ + e₂).repr < e₁.repr + b₂
⊢ ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)

Tactic:
apply NFBelow.oadd

Premises used: ONote.NFBelow.oadd
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
⊢ (e₁ + e₂).NF

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
neg neg₁ neg₂ neg₃ : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
⊢ (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁ + e₂).repr

Tactic:
rwa [repr_add]

Premises used: ONote.repr_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
neg : e₂.repr < b₂
⊢ (e₁ + e₂).repr < e₁.repr + b₂

Tactic:
rw [repr_add, add_lt_add_iff_left]

Premises used: ONote.repr_add, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
⊢ e₂.repr < b₂

Tactic:
h₂.lt

Premises used: ONote.NFBelow.lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
⊢ e₂.repr < b₂

Tactic:
exact h₂.lt

Premises used: ONote.NFBelow.lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
h : NF 0
h₂ : o.NF
zero : ∀ (h₂ : ONote.zero.NF), (0 * ONote.zero).NF
oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote) (h₂ : (a.oadd a_1 a_2).NF), (0 * a.oadd a_1 a_2).NF
⊢ (0 * o).NF

Tactic:
cases o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
h₂ : zero.NF
⊢ (0 * zero).NF

Tactic:
NF.zero

Premises used: ONote.mul, ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
h₂ : zero.NF
⊢ (0 * zero).NF

Tactic:
exact NF.zero

Premises used: ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
a : ONote
a_1 : ℕ+
a_2 : ONote
h₂ : (a.oadd a_1 a_2).NF
⊢ (0 * a.oadd a_1 a_2).NF

Tactic:
NF.zero

Premises used: ONote.mul, ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
a : ONote
a_1 : ℕ+
a_2 : ONote
h₂ : (a.oadd a_1 a_2).NF
⊢ (0 * a.oadd a_1 a_2).NF

Tactic:
exact NF.zero

Premises used: ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
h : NF 0
h₂ : o.NF
zero : ∀ (h₂ : ONote.zero.NF), (0 * ONote.zero).repr = repr 0 * ONote.zero.repr
oadd :
  ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote) (h₂ : (a.oadd a_1 a_2).NF),
    (0 * a.oadd a_1 a_2).repr = repr 0 * (a.oadd a_1 a_2).repr
⊢ (0 * o).repr = repr 0 * o.repr

Tactic:
cases o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
h₂ : zero.NF
⊢ (0 * zero).repr = repr 0 * zero.repr

Tactic:
(zero_mul _).symm

Premises used: MulZeroClass.zero_mul, ONote.repr, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
h₂ : zero.NF
⊢ (0 * zero).repr = repr 0 * zero.repr

Tactic:
exact (zero_mul _).symm

Premises used: MulZeroClass.zero_mul, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
a : ONote
a_1 : ℕ+
a_2 : ONote
h₂ : (a.oadd a_1 a_2).NF
⊢ (0 * a.oadd a_1 a_2).repr = repr 0 * (a.oadd a_1 a_2).repr

Tactic:
(zero_mul _).symm

Premises used: MulZeroClass.zero_mul, ONote.repr, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
a : ONote
a_1 : ℕ+
a_2 : ONote
h₂ : (a.oadd a_1 a_2).NF
⊢ (0 * a.oadd a_1 a_2).repr = repr 0 * (a.oadd a_1 a_2).repr

Tactic:
exact (zero_mul _).symm

Premises used: MulZeroClass.zero_mul, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
⊢ ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr

Tactic:
have IH : repr (mul _ _) = _ := @repr_mul _ _ h₁ h₂.snd
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
lhs : (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr
| (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
lhs