awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ : ℕ)
nh : (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.gt
⊢ (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.gt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.gt

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
left : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nh : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.gt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.gt
inr :
  ∀ (nh : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = 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₁ : ℕ) ∧ 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
left : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nh : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = 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:
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
left : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nh : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = 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:
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
left : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nh : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = 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
left_1 : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nh : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.gt
left : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ)
⊢ Ordering.eq = 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₁ : ℕ)
left_1 : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ)
right : 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)

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.gt ∨
    (↑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)

Tactic:
case gt =>
        rcases nh with nh | nh
        · cases nh; contradiction
        · obtain ⟨_, nh⟩ := nh
          rw [ite_eq_iff] at nh; rcases nh with nh | nh
          · exact oadd_lt_oadd_2 h₂ nh.left
          · 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.eq ∨
    (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.eq
eq :
  ∀ (nh : (↑n₁ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.lt = 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)
eq₁ :
  ∀ (nh : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = 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)
⊢ (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)

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.eq
⊢ (↑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.eq
left : (↑n₁ : ℕ) < (↑n₂ : ℕ)
⊢ Ordering.lt = Ordering.eq

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.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)

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.eq
⊢ (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)

Tactic:
obtain ⟨nhl, nhr⟩ := 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.eq
nhl : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
⊢ (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.eq

Tactic:
obtain ⟨nhl, nhr⟩ := 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
nhl : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nhr : (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.eq
⊢ (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.eq ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.eq

Tactic:
rw [ite_eq_iff] at nhr

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
nhl : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nhr : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.eq ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.eq
eq :
  ∀ (nhr : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = 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)
eq₁ :
  ∀ (nhr : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = 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)
⊢ (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)

Tactic:
rcases nhr with nhr | nhr
-- 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
nhl : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nhr : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.eq
⊢ (↑n₂ : ℕ) < (↑n₁ : ℕ)

Tactic:
cases nhr
-- 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
nhl : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nhr : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.eq
left : (↑n₂ : ℕ) < (↑n₁ : ℕ)
⊢ Ordering.gt = Ordering.eq

Tactic:
cases nhr
-- 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
nhl : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
left : (↑n₂ : ℕ) < (↑n₁ : ℕ)
right : Ordering.gt = 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)

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
nhl : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.eq
eq :
  ∀ (h : o₁ = e₁.oadd n₂ a₁) (h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h).NF) (nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ))
    (nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = 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)
⊢ (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)

Tactic:
obtain rfl := Subtype.ext (nhl.eq_of_not_lt nhr.1)

Premises used: LE.le.eq_of_not_lt, And.left, rfl, Subtype.ext
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
⊢ (a₁.cmp a₂).Compares a₁ a₂

Tactic:
have IHa := @cmp_compares _ _ h₁.snd h₂.snd
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
IHa : (a₁.cmp a₂).Compares a₁ a₂
eq :
  ∀ (IHa : (a₁.cmp a₂).Compares a₁ a₂),
    (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h)
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h)

Tactic:
revert IHa
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
eq :
  ∀ (IHa : Ordering.lt.Compares a₁ a₂),
    (Ordering.eq.then (Ordering.eq.then Ordering.lt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h)
eq₁ :
  ∀ (IHa : Ordering.eq.Compares a₁ a₂),
    (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h)
eq₂ :
  ∀ (IHa : Ordering.gt.Compares a₁ a₂),
    (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h)
⊢ ∀ (IHa : (a₁.cmp a₂).Compares a₁ a₂),
    (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h)

Tactic:
cases cmp a₁ a₂

Premises used: ONote.cmp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
IHa : a₁ < a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.lt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h)

Tactic:
oadd_lt_oadd_3 IHa

Premises used: ONote.oadd_lt_oadd_3, Ordering.Compares
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
IHa : a₁ < a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.lt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h)

Tactic:
exact oadd_lt_oadd_3 IHa

Premises used: ONote.oadd_lt_oadd_3
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
IHa : a₁ < a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.lt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h)

Tactic:
case lt => exact oadd_lt_oadd_3 IHa

Premises used: ONote.oadd_lt_oadd_3
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
IHa : a₁ > a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h)

Tactic:
oadd_lt_oadd_3 IHa

Premises used: ONote.oadd_lt_oadd_3, Ordering.Compares
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
IHa : a₁ > a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h)

Tactic:
exact oadd_lt_oadd_3 IHa

Premises used: ONote.oadd_lt_oadd_3
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
IHa : a₁ > a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h)

Tactic:
case gt => exact oadd_lt_oadd_3 IHa

Premises used: ONote.oadd_lt_oadd_3
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : o₂ = e₁.oadd n₂ a₂
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
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
IHa : a₁ = a₂
eq :
  ∀ (h : o₂ = e₁.oadd n₂ a₁) (h₂ : (namedPattern o₂ (e₁.oadd n₂ a₁) h).NF),
    (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
      (namedPattern o₂ (e₁.oadd n₂ a₁) h)
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h_1)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h)

Tactic:
subst IHa
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
h : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h).NF
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
h_1 : o₂ = e₁.oadd n₂ a₁
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₁) h_1).NF
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₁) h_1)

Tactic:
rfl

Premises used: Ordering.Compares, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
h : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h).NF
nhl : (↑n₂ : ℕ) ≤ (↑n₂ : ℕ)
nhr : ¬(↑n₂ : ℕ) < (↑n₂ : ℕ) ∧ Ordering.eq = Ordering.eq
h_1 : o₂ = e₁.oadd n₂ a₁
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₁) h_1).NF
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₁) h_1)

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a b : ONote
inst : a.NF
inst_1 : b.NF
⊢ a.repr = b.repr ↔ a = b

Tactic:
⟨fun e => match cmp a b, cmp_compares a b with
    | Ordering.lt, (h : repr a < repr b) => (ne_of_lt h e).elim
    | Ordering.gt, (h : repr a > repr b)=> (ne_of_gt h e).elim
    | Ordering.eq, h => h,
    congr_arg _⟩

Premises used: ONote.cmp_compares, False.elim, ONote.cmp, ne_of_gt, congr_arg, _private.0.ONote.repr_inj.match_1, Iff.intro, ne_of_lt, Eq
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h_1 : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
h : e.oadd n a = 0
⊢ False

Tactic:
injection h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
⊢ ¬(e.oadd n a).repr = repr 0

Tactic:
have := mt repr_inj.1 (fun h => by injection h : ONote.oadd e n a ≠ 0)
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
this : ¬(e.oadd n a).repr = repr 0
⊢ b ≤ e.repr

Tactic:
have L := le_of_not_gt fun l => not_le_of_gt (h.below_of_lt l).repr_lt (le_of_dvd this d)
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
this : ¬(e.oadd n a).repr = repr 0
L : b ≤ e.repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Tactic:
⟨L, (dvd_add_iff <| (opow_dvd_opow _ L).mul_right _).1 d⟩

Premises used: Ordinal.dvd_add_iff, Dvd.dvd.mul_right, Ordinal.opow_dvd_opow, And.intro, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr
this : ¬(e.oadd n a).repr = repr 0
L : b ≤ e.repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Tactic:
exact ⟨L, (dvd_add_iff <| (opow_dvd_opow _ L).mul_right _).1 d⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
rw : HPow.hPow (β := Ordinal.{0}) ω 1 ∣ (e.oadd n a).repr → 1 ≤ e.repr ∧ HPow.hPow (β := Ordinal.{0}) ω 1 ∣ a.repr
⊢ ω ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ ω ∣ a.repr

Tactic:
rw [← opow_one ω, ← one_le_iff_ne_zero]

Premises used: Ordinal.opow_one, Ordinal.omega0, Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ HPow.hPow (β := Ordinal.{0}) ω 1 ∣ (e.oadd n a).repr → 1 ≤ e.repr ∧ HPow.hPow (β := Ordinal.{0}) ω 1 ∣ a.repr

Tactic:
h.of_dvd_omega0_opow

Premises used: ONote.NF.of_dvd_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ HPow.hPow (β := Ordinal.{0}) ω 1 ∣ (e.oadd n a).repr → 1 ≤ e.repr ∧ HPow.hPow (β := Ordinal.{0}) ω 1 ∣ a.repr

Tactic:
exact h.of_dvd_omega0_opow

Premises used: ONote.NF.of_dvd_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b o : ONote
zero : Decidable (b.TopBelow ONote.zero)
oadd : (a : ONote) → (a_1 : ℕ+) → (a_2 : ONote) → Decidable (b.TopBelow (a.oadd a_1 a_2))
⊢ Decidable (b.TopBelow o)

Tactic:
cases o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b : ONote
⊢ Decidable
    (match (motive := ONote → Prop) zero with
    | zero => True
    | e.oadd a a_1 => e.cmp b = Ordering.lt)

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
b a : ONote
a_1 : ℕ+
a_2 : ONote
⊢ Decidable
    (match (motive := ONote → Prop) a.oadd a_1 a_2 with
    | zero => True
    | e.oadd a a_3 => e.cmp b = Ordering.lt)

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
have : (this : Decidable e.NF) → Decidable (e.oadd n a).NF
⊢ Decidable (e.oadd n a).NF

Tactic:
have := decidableNF e
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
this : Decidable e.NF
have : (this : Decidable a.NF) → Decidable (e.oadd n a).NF
⊢ Decidable (e.oadd n a).NF

Tactic:
have := decidableNF a
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
this_1 : Decidable e.NF
this : Decidable a.NF
h : e.NF ∧ a.NF ∧ e.TopBelow a ↔ (e.oadd n a).NF
⊢ Decidable (e.oadd n a).NF

Tactic:
apply decidable_of_iff (NF e ∧ NF a ∧ TopBelow e a)

Premises used: ONote.NF, decidable_of_iff, And, ONote.TopBelow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
this_1 : Decidable e.NF
this : Decidable a.NF
h : e.NF ∧ a.NFBelow e.repr ↔ (e.oadd n a).NF
⊢ e.NF ∧ a.NF ∧ e.TopBelow a ↔ (e.oadd n a).NF

Tactic:
rw [← and_congr_right fun h => @nfBelow_iff_topBelow _ h _]

Premises used: ONote.nfBelow_iff_topBelow, and_congr_right
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
this_1 : Decidable e.NF
this : Decidable a.NF
⊢ e.NF ∧ a.NFBelow e.repr ↔ (e.oadd n a).NF

Tactic:
⟨fun ⟨h₁, h₂⟩ => NF.oadd h₁ n h₂, fun h => ⟨h.fst, h.snd'⟩⟩

Premises used: ONote.NF, ONote.oadd, ONote.NF.oadd, And.intro, ONote.NF.fst, Iff.intro, ONote.decidableNF.match_1, ONote.NF.snd'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
this_1 : Decidable e.NF
this : Decidable a.NF
⊢ e.NF ∧ a.NFBelow e.repr ↔ (e.oadd n a).NF

Tactic:
exact ⟨fun ⟨h₁, h₂⟩ => NF.oadd h₁ n h₂, fun h => ⟨h.fst, h.snd'⟩⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
⊢ 0 + o = o

Tactic:
rfl

Premises used: ONote.add, rfl