awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ (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)
have 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)
Tactic: rcases nh.right with nh | nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ (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)
have 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)
Tactic: rcases nh.right with nh | nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have left : (↑n₂ : ℕ) < (↑n₁ : ℕ)
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
have right : Ordering.gt = Ordering.lt
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have left : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ)
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
have right : Ordering.eq = Ordering.lt
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
have 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)
Tactic: rcases nh with nh | nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ (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)
have 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)
Tactic: rcases nh with nh | nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have left : (↑n₁ : ℕ) < (↑n₂ : ℕ)
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
have right : Ordering.lt = Ordering.gt
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have left : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
Tactic: obtain ⟨_, nh⟩ := nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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₁ : ℕ)
⊢ (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)
have nh₁ : (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.gt
Tactic: obtain ⟨_, nh⟩ := nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have nh₁ : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.gt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.gt
Tactic: rw [ite_eq_iff] at nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ (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)
have 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)
Tactic: rcases nh with nh | nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ (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)
have 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)
Tactic: rcases nh with nh | nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have left : ¬(↑n₂ : ℕ) < (↑n₁ : ℕ)
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
have right : Ordering.eq = Ordering.gt
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ (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)
have 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)
Tactic: rcases nh with nh | nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ (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)
have 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)
Tactic: rcases nh with nh | nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have left : (↑n₁ : ℕ) < (↑n₂ : ℕ)
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
have right : Ordering.lt = Ordering.eq
Tactic: cases nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have nhl : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ)
Tactic: obtain ⟨nhl, nhr⟩ := nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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₁ : ℕ)
⊢ (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)
have nhr : (if (↑n₂ : ℕ) < (↑n₁ : ℕ) then Ordering.gt else Ordering.eq) = Ordering.eq
Tactic: obtain ⟨nhl, nhr⟩ := nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have nhr₁ : (↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.eq ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.eq
Tactic: rw [ite_eq_iff] at nhr
Cleared hypotheses: nhr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ (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)
have 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)
Tactic: rcases nhr with nhr | nhr
Cleared hypotheses: nhr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ (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)
have 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)
Tactic: rcases nhr with nhr | nhr
Cleared hypotheses: nhr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have left : (↑n₂ : ℕ) < (↑n₁ : ℕ)
Tactic: cases nhr
Cleared hypotheses: nhr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h_1)
have right : Ordering.gt = Ordering.eq
Tactic: cases nhr
Cleared hypotheses: nhr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ (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)
have 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)
Tactic: obtain rfl := Subtype.ext (nhl.eq_of_not_lt nhr.1)
Cleared hypotheses: n₁, h, h₁, nhl, nhr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ (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)
have IHa : (a₁.cmp a₂).Compares a₁ a₂
Tactic: have IHa := @cmp_compares _ _ h₁.snd h₂.snd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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₂
⊢ (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)
have 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)
Tactic: revert IHa
Cleared hypotheses: IHa
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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₂),
    (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)
have 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)
Tactic: cases cmp a₁ a₂