awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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 : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr ≤ ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0})

Tactic:
simpa using (mul_le_mul_iff_right₀ <| opow_pos (repr e') omega0_pos).2
          (Nat.cast_le.2 n'.pos)

Premises used: Iff.mpr, Ordinal.omega0_pos, PNat.pos, ONote.repr, Nat.cast_le, Ordinal.opow_pos, mul_le_mul_iff_right₀
-- 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.eq
ee : e = e'
oadd :
  ω ^ 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)
oadd₁ :
  ω ^ 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
oadd₂ oadd₃ :
  ω ^ e'.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr =
    ω ^ e'.repr * HAdd.hAdd (α := Ordinal.{0}) (↑(↑n : ℕ) : Ordinal.{0}) (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr
⊢ ω ^ 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)

Tactic:
rw [ee, ← add_assoc, ← mul_add]

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

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

Tactic:
NFBelow.zero

Premises used: ONote.sub, ONote.NFBelow.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
h : NFBelow 0 b
h₂ : zero.NF
⊢ (0 - zero).NFBelow b

Tactic:
exact NFBelow.zero

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

Tactic:
NFBelow.zero

Premises used: ONote.sub, ONote.NFBelow.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
h : NFBelow 0 b
a : ONote
a_1 : ℕ+
a_2 : ONote
h₂ : (a.oadd a_1 a_2).NF
⊢ (0 - a.oadd a_1 a_2).NFBelow b

Tactic:
exact NFBelow.zero

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

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

Tactic:
simp only [HSub.hSub, Sub.sub, sub] at h' ⊢

Premises used: ONote.sub, HSub.hSub, Sub.sub
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
⊢ (e₁.cmp e₂).Compares e₁ e₂

Tactic:
have := @cmp_compares _ _ h₁.fst h₂.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
lt :
  ∀ (h : e₁.cmp e₂ = Ordering.lt),
    NFBelow
      (match (motive := Ordering → ONote) Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁)
      b
eq :
  ∀ (h : e₁.cmp e₂ = Ordering.eq),
    NFBelow
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁)
      b
gt :
  ∀ (h : e₁.cmp e₂ = Ordering.gt),
    NFBelow
      (match (motive := Ordering → ONote) Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁)
      b
⊢ NFBelow
    (match (motive := Ordering → ONote) e₁.cmp e₂ with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b

Tactic:
cases h : cmp e₁ e₂

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

Tactic:
apply NFBelow.zero

Premises used: ONote.NFBelow.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.eq
eq :
  NFBelow
    (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₁)
    b
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b

Tactic:
rw [Nat.sub_eq]

Premises used: Nat.sub_eq
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.eq
⊢ e₁ = e₂

Tactic:
simp only [h, Ordering.compares_eq] at this

Premises used: Ordering.compares_eq
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
h : e₁.cmp e₂ = Ordering.eq
this : e₁ = e₂
⊢ (e₁.oadd n₂ a₂).NF

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

Tactic:
subst e₂
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
eq :
  NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) 0 with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b
eq₁ :
  ∀ (n : ℕ),
    NFBelow
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) n + 1 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁)
      b
⊢ NFBelow
    (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₁)
    b

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

Premises used: PNat.val
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
pos :
  ∀ (en : n₁ = n₂),
    NFBelow
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) 0 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁)
      b
neg :
  ∀ (en : ¬n₁ = n₂),
    NFBelow
      (match (motive := Ordering → ONote) Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (motive := ℕ → ONote) 0 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁)
      b
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) 0 with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b

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

Tactic:
simp only [en, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : ¬n₁ = n₂
neg : NFBelow 0 b
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) 0 with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b

Tactic:
simp only [en, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : n₁ = n₂
⊢ (a₁.sub a₂).NFBelow b

Tactic:
h'.mono (le_of_lt h₁.lt)

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

Tactic:
exact h'.mono (le_of_lt h₁.lt)

Premises used: le_of_lt, ONote.NFBelow.lt, ONote.NFBelow.mono
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : ¬n₁ = n₂
⊢ NFBelow 0 b

Tactic:
NFBelow.zero

Premises used: ONote.NFBelow.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : ¬n₁ = n₂
⊢ NFBelow 0 b

Tactic:
exact NFBelow.zero

Premises used: ONote.NFBelow.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) n + 1 with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    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:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.eq with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) n + 1 with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    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:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.gt
⊢ NFBelow
    (match (motive := Ordering → ONote) Ordering.gt with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match (motive := ℕ → ONote) (↑n₁ : ℕ).sub (↑n₂ : ℕ) with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁)
    b

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

Tactic:
exact h₁
-- 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:
(Ordinal.zero_sub _).symm

Premises used: Ordinal.zero_sub, 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 (Ordinal.zero_sub _).symm

Premises used: Ordinal.zero_sub, 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:
(Ordinal.zero_sub _).symm

Premises used: Ordinal.zero_sub, 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 (Ordinal.zero_sub _).symm

Premises used: Ordinal.zero_sub, 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
⊢ a₁.NF

Tactic:
haveI := 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
this : a₁.NF
⊢ a₂.NF

Tactic:
haveI := 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
this_1 : a₁.NF
this : a₂.NF
⊢ (a₁ - a₂).repr = a₁.repr - a₂.repr

Tactic:
have h' := repr_sub a₁ a₂
-- 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₁ - a₂).repr = a₁.repr - a₂.repr
⊢ (a₁.sub a₂).repr = a₁.repr - a₂.repr

Tactic:
conv_lhs at h' => dsimp [HSub.hSub, Sub.sub, sub]

Premises used: ONote.sub, HSub.hSub, Sub.sub
-- 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
dsimp :
  repr
    (match (motive := Ordering → ONote) e₁.cmp e₂ 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₁).sub (e₂.oadd n₂ a₂)).repr

Tactic:
dsimp only [sub]

Premises used: ONote.sub
-- 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
dsimp :
  repr
    (match (motive := Ordering → ONote) e₁.cmp e₂ 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₁ - e₂.oadd n₂ a₂).repr

Tactic:
dsimp only [HSub.hSub, Sub.sub]; dsimp only [sub]

Premises used: ONote.sub, HSub.hSub, Sub.sub
-- 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
conv_lhs :
  repr
      (match (motive := Ordering → ONote) e₁.cmp e₂ 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
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
conv_lhs => dsimp only [HSub.hSub, Sub.sub]; dsimp only [sub]

Premises used: ONote.sub, HSub.hSub, Sub.sub
-- 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
⊢ (e₁.cmp e₂).Compares e₁ e₂

Tactic:
have ee := @cmp_compares _ _ h₁.fst h₂.fst
-- 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
ee : (e₁.cmp e₂).Compares e₁ e₂
lt :
  ∀ (h : e₁.cmp e₂ = Ordering.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₁) =
      (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
eq :
  ∀ (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
gt :
  ∀ (h : e₁.cmp e₂ = Ordering.gt),
    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
⊢ repr
      (match (motive := Ordering → ONote) e₁.cmp e₂ 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:
cases h : cmp e₁ e₂

Premises used: ONote.cmp
-- 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
ee : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.lt
⊢ Ordering.lt.Compares e₁ e₂

Tactic:
simp only [h] 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
ee : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.eq
⊢ Ordering.eq.Compares e₁ e₂

Tactic:
simp only [h] 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
ee : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.gt
⊢ Ordering.gt.Compares e₁ e₂

Tactic:
simp only [h] at ee