awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : (↑n₁ : ℕ) < (↑n₂ : ℕ)
⊢ ω ^ e.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + o₁.repr < ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) + o₂.repr

Tactic:
(add_lt_add_right h₁.snd'.repr_lt _).trans_le (le_trans ?_ le_self_add)

Premises used: add_lt_add_right, LT.lt.trans_le, le_self_add, ONote.NF.snd', ONote.NFBelow.repr_lt, le_trans
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : (↑n₁ : ℕ) < (↑n₂ : ℕ)
refine : ω ^ e.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})
⊢ ω ^ e.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + o₁.repr < ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) + o₂.repr

Tactic:
refine (add_lt_add_right h₁.snd'.repr_lt _).trans_le (le_trans ?_ le_self_add)

Premises used: add_lt_add_right, LT.lt.trans_le, le_self_add, ONote.NF.snd', ONote.NFBelow.repr_lt, le_trans
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : (↑n₁ : ℕ) < (↑n₂ : ℕ)
rwa : ω ^ e.repr * succ (↑(↑n₁ : ℕ) : Ordinal.{0}) ≤ ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})
rwa₁ : LE.le (α := Ordinal.{0}) (succ (↑(↑n₁ : ℕ) : Ordinal.{0})) (↑(↑n₂ : ℕ) : Ordinal.{0})
rwa₂ : LT.lt (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑(↑n₂ : ℕ) : Ordinal.{0})
rwa₃ rwa₄ rwa₅ rwa₆ : (↑n₁ : ℕ) < (↑n₂ : ℕ)
⊢ ω ^ e.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})

Tactic:
rwa [← mul_succ, mul_le_mul_iff_right₀ (opow_pos _ omega0_pos), succ_le_iff, Nat.cast_lt]

Premises used: Ordinal.omega0_pos, Ordinal.mul_succ, Order.succ_le_iff, Nat.cast_lt, Ordinal.opow_pos, mul_le_mul_iff_right₀
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a₁.repr < ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a₂.repr

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
⊢ (e₁.cmp e₂).Compares e₁ e₂

Tactic:
have IHe := @cmp_compares _ _ h₁.fst h₂.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
IHe : (e₁.cmp e₂).Compares e₁ e₂
⊢ match (motive := Ordering → ONote → ONote → Prop) e₁.cmp e₂, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a

Tactic:
simp only [Ordering.Compares, gt_iff_lt] at IHe

Premises used: Ordering.Compares, gt_iff_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
IHe :
  match (motive := Ordering → ONote → ONote → Prop) e₁.cmp e₂, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
revert :
  ∀
    (IHe :
      match (motive := Ordering → ONote → ONote → Prop) e₁.cmp e₂, e₁, e₂ with
      | Ordering.lt, a, b => a < b
      | Ordering.eq, a, b => a = b
      | Ordering.gt, a, b => b < a),
    ((e₁.cmp e₂).then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)
⊢ ((e₁.cmp e₂).then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)

Tactic:
revert IHe
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
cases :
  ∀
    (IHe :
      match (motive := Ordering → ONote → ONote → Prop) Ordering.lt, e₁, e₂ with
      | Ordering.lt, a, b => a < b
      | Ordering.eq, a, b => a = b
      | Ordering.gt, a, b => b < a),
    (Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)
cases₁ :
  ∀
    (IHe :
      match (motive := Ordering → ONote → ONote → Prop) Ordering.eq, e₁, e₂ with
      | Ordering.lt, a, b => a < b
      | Ordering.eq, a, b => a = b
      | Ordering.gt, a, b => b < a),
    (Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)
cases₂ :
  ∀
    (IHe :
      match (motive := Ordering → ONote → ONote → Prop) Ordering.gt, e₁, e₂ with
      | Ordering.lt, a, b => a < b
      | Ordering.eq, a, b => a = b
      | Ordering.gt, a, b => b < a),
    (Ordering.gt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)
⊢ ∀
    (IHe :
      match (motive := Ordering → ONote → ONote → Prop) e₁.cmp e₂, e₁, e₂ with
      | Ordering.lt, a, b => a < b
      | Ordering.eq, a, b => a = b
      | Ordering.gt, a, b => b < a),
    ((e₁.cmp e₂).then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)

Tactic:
cases cmp e₁ e₂

Premises used: ONote.cmp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
IHe :
  match (motive := Ordering → ONote → ONote → Prop) Ordering.lt, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)

Tactic:
oadd_lt_oadd_1 h₁ IHe

Premises used: ONote.oadd_lt_oadd_1, Ordering.Compares
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
IHe :
  match (motive := Ordering → ONote → ONote → Prop) Ordering.lt, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)

Tactic:
exact oadd_lt_oadd_1 h₁ IHe

Premises used: ONote.oadd_lt_oadd_1
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
⊢ ∀
    (IHe :
      match (motive := Ordering → ONote → ONote → Prop) Ordering.lt, e₁, e₂ with
      | Ordering.lt, a, b => a < b
      | Ordering.eq, a, b => a = b
      | Ordering.gt, a, b => b < a),
    (Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)

Tactic:
case lt => intro IHe; exact oadd_lt_oadd_1 h₁ IHe
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
IHe :
  match (motive := Ordering → ONote → ONote → Prop) Ordering.gt, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.gt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)

Tactic:
oadd_lt_oadd_1 h₂ IHe

Premises used: ONote.oadd_lt_oadd_1, Ordering.Compares
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
IHe :
  match (motive := Ordering → ONote → ONote → Prop) Ordering.gt, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.gt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)

Tactic:
exact oadd_lt_oadd_1 h₂ IHe

Premises used: ONote.oadd_lt_oadd_1
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
⊢ ∀
    (IHe :
      match (motive := Ordering → ONote → ONote → Prop) Ordering.gt, e₁, e₂ with
      | Ordering.lt, a, b => a < b
      | Ordering.eq, a, b => a = b
      | Ordering.gt, a, b => b < a),
    (Ordering.gt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)

Tactic:
case gt => intro IHe; exact oadd_lt_oadd_1 h₂ IHe
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h_1 : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h_1).NF
IHe : e₁ = e₂
subst :
  ∀ (h_2 : o₂ = e₁.oadd n₂ a₂) (h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_2).NF),
    (Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_2)
⊢ (Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h_1)

Tactic:
subst IHe
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
lt :
  ∀ (nh : cmpUsing (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.lt),
    (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
eq :
  ∀ (nh : cmpUsing (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq),
    (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
gt :
  ∀ (nh : cmpUsing (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.gt),
    (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
⊢ (Ordering.eq.then ((cmpUsing (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂))).Compares
    (namedPattern o₁ (e₁.oadd n₁ a₁) h) (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
cases nh : cmpUsing (· < ·) (n₁ : ℕ) n₂

Premises used: PNat.val, cmpUsing, LT.lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : cmpUsing (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.lt
⊢ (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.lt ∨
    (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.lt

Tactic:
rw [cmpUsing, ite_eq_iff, not_lt] at nh

Premises used: cmpUsing, not_lt, ite_eq_iff
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : cmpUsing (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq
⊢ (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.eq ∨
    (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.eq

Tactic:
rw [cmpUsing, ite_eq_iff, not_lt] at nh

Premises used: cmpUsing, not_lt, ite_eq_iff
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : cmpUsing (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.gt
⊢ (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.gt ∨
    (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.gt

Tactic:
rw [cmpUsing, ite_eq_iff, not_lt] at nh

Premises used: cmpUsing, not_lt, ite_eq_iff
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh :
  (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.lt ∨
    (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.lt
inl :
  ∀ (nh : (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.lt),
    (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
inr :
  ∀ (nh : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.lt),
    (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
rcases nh with nh | nh
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
oadd_lt_oadd_2 h₁ nh.left

Premises used: Ordering.Compares, And.left, ONote.oadd_lt_oadd_2
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
exact oadd_lt_oadd_2 h₁ nh.left

Premises used: And.left, ONote.oadd_lt_oadd_2
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.lt
⊢ (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧
    ((↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt)

Tactic:
rw [ite_eq_iff] at nh

Premises used: ite_eq_iff
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh :
  (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧
    ((↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt)
inr :
  ∀ (nh : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt),
    (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
inr₁ :
  ∀ (nh : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt),
    (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
rcases nh.right with nh | nh

Premises used: And.right
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh_1 :
  (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧
    ((↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt)
nh : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt
⊢ (↑n₂ : ℕ) < (↑n₁ : ℕ)

Tactic:
cases nh
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh_1 :
  (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧
    ((↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt)
nh : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt
left : (↑n₂ : ℕ) < (↑n₁ : ℕ)
⊢ Ordering.gt = Ordering.lt

Tactic:
cases nh
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh_1 :
  (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧
    ((↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt)
nh : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt
⊢ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ)

Tactic:
cases nh
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh_1 :
  (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧
    ((↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt)
nh : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt
left : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ)
⊢ Ordering.eq = Ordering.lt

Tactic:
cases nh
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh :
  (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧
    ((↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt)
left : (↑n₂ : ℕ) < (↑n₁ : ℕ)
right : Ordering.gt = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
contradiction
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh :
  (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧
    ((↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt)
left : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ)
right : Ordering.eq = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
contradiction
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh :
  (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.lt ∨
    (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
case lt =>
        rcases nh with nh | nh
        · exact oadd_lt_oadd_2 h₁ nh.left
        · rw [ite_eq_iff] at nh; rcases nh.right with nh | nh <;> cases nh <;> contradiction

Premises used: ite_eq_iff
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh :
  (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.gt ∨
    (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.gt
inl :
  ∀ (nh : (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.gt),
    (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
inr :
  ∀ (nh : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.gt),
    (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
rcases nh with nh | nh
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.gt
⊢ (↑n₁ : ℕ) < (↑n₂ : ℕ)

Tactic:
cases nh
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = Ordering.gt
left : (↑n₁ : ℕ) < (↑n₂ : ℕ)
⊢ Ordering.lt = Ordering.gt

Tactic:
cases nh
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
left : (↑n₁ : ℕ) < (↑n₂ : ℕ)
right : Ordering.lt = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)

Tactic:
contradiction
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.gt
⊢ (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)

Tactic:
obtain ⟨_, nh⟩ := nh
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h).NF
h_1 : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_1).NF
nh : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.gt
left : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
⊢ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.gt

Tactic:
obtain ⟨_, nh⟩ := nh