awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ 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
have 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
Tactic: cases (n₁ : ℕ) - n₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ 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
have 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: cases (n₁ : ℕ) - n₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ 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
have 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
Tactic: by_cases en : n₁ = n₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ 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
have 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
Tactic: by_cases en : n₁ = n₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
    (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
have pos : (a₁.sub a₂).NFBelow b
Tactic: simp only [en, ↓reduceIte]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
    (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
have neg : NFBelow 0 b
Tactic: simp only [en, ↓reduceIte]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
h : NF 0
h₂ : o.NF
⊢ (0 - o).repr = repr 0 - o.repr
have zero : ∀ (h₂ : zero.NF), (0 - zero).repr = repr 0 - zero.repr
Tactic: cases o
Cleared hypotheses: o, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
h : NF 0
h₂ : o.NF
zero : ∀ (h₂ : ONote.zero.NF), (0 - ONote.zero).repr = repr 0 - ONote.zero.repr
⊢ (0 - o).repr = repr 0 - o.repr
have 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
Tactic: cases o
Cleared hypotheses: o, h₂
-- 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
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
have this : a₁.NF
Tactic: haveI := h₁.snd
-- 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
this : a₁.NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
have this₁ : a₂.NF
Tactic: haveI := h₂.snd
-- 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
this_1 : a₁.NF
this : a₂.NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
have h' : (a₁ - a₂).repr = a₁.repr - a₂.repr
Tactic: have h' := repr_sub a₁ a₂
-- 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
this_1 : a₁.NF
this : a₂.NF
h' : (a₁ - a₂).repr = a₁.repr - a₂.repr
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
have h'₁ : (a₁.sub a₂).repr = a₁.repr - a₂.repr
Tactic: conv_lhs at h' => dsimp [HSub.hSub, Sub.sub, sub]
Cleared hypotheses: h'
-- 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
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
| ((e₁.oadd n₁ a₁).sub (e₂.oadd n₂ a₂)).repr
have 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₁)
Tactic: dsimp only [sub]
-- 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
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
| (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr
have 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₁)
Tactic: dsimp only [HSub.hSub, Sub.sub]; dsimp only [sub]
-- 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
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
have 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
Tactic: conv_lhs => dsimp only [HSub.hSub, Sub.sub]; dsimp only [sub]
-- 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
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - 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
have ee : (e₁.cmp e₂).Compares e₁ e₂
Tactic: have ee := @cmp_compares _ _ h₁.fst h₂.fst
-- 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
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
ee : (e₁.cmp e₂).Compares e₁ e₂
⊢ 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
have 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
Tactic: cases h : cmp e₁ e₂
-- 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
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
⊢ 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
have 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
Tactic: cases h : cmp e₁ e₂
-- 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
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
⊢ 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
have 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
Tactic: cases h : cmp e₁ e₂
-- 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
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
⊢ 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
have ee₁ : Ordering.lt.Compares e₁ e₂
Tactic: simp only [h] at ee
Cleared hypotheses: ee
-- 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
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
⊢ 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
have ee₁ : Ordering.eq.Compares e₁ e₂
Tactic: simp only [h] at ee
Cleared hypotheses: ee
-- 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
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
⊢ 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
have ee₁ : Ordering.gt.Compares e₁ e₂
Tactic: simp only [h] at ee
Cleared hypotheses: ee
-- 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
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₁) =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
have 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
Tactic: rw [Ordinal.sub_eq_zero_iff_le.2]
-- 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
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
⊢ 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
have lt₁ : (e₁.oadd n₁ a₁).repr ≤ (e₂.oadd n₂ a₂).repr
Tactic: rw [Ordinal.sub_eq_zero_iff_le.2]
-- 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
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₂
⊢ 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
have ee₁ : e₁ = e₂
Tactic: change e₁ = e₂ at ee
Cleared hypotheses: ee
-- 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
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₂
⊢ 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
have 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
Tactic: subst e₂
Cleared hypotheses: e₂, h₂, h, ee
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ 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
have 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
Tactic: cases mn : (n₁ : ℕ) - n₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ 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
have 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
Tactic: cases mn : (n₁ : ℕ) - n₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
have pos : ∀ (en : n₁ = n₂), (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₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
have neg : ∀ (en : ¬n₁ = n₂), (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₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
have neg : repr 0 = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
Tactic: simp only [en, ite_false]