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
h₁ : e₁.cmp e₁ = Ordering.eq
eq :
  ∀ (h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.lt)
    (h : Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
eq₁ :
  ∀ (h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq)
    (h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
⊢ ∀ (h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
have eq₂ : ∀ (h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.gt)
  (h : Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
Tactic: cases h₂ : _root_.cmp (n₁ : ℕ) n₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
have eq : ∀ (h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁
Tactic: obtain rfl := eq_of_cmp_eq h
Cleared hypotheses: a₂, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁
have h₃ : (↑n₂ : ℕ) = (↑n₁ : ℕ)
Tactic: rw [_root_.cmp, cmpUsing_eq_eq, not_lt, not_lt, ← le_antisymm_iff] at h₂
Cleared hypotheses: h₂, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : (↑n₂ : ℕ) = (↑n₁ : ℕ)
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁
have eq : ∀ (h₂ : (↑n₂ : ℕ) = (↑n₂ : ℕ)), e₁.oadd n₂ a₁ = e₁.oadd n₂ a₁
Tactic: obtain rfl := Subtype.ext h₂
Cleared hypotheses: n₁, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ e.NF
have oadd' : ∀ {eb : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b), e.NF
Tactic: obtain - | ⟨h₁, h₂, h₃⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ a.NFBelow e.repr
have oadd' : ∀ {eb : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b), a.NFBelow e.repr
Tactic: obtain - | ⟨h₁, h₂, h₃⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ e.repr < b
have oadd' : ∀ {eb : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b), e.repr < b
Tactic: obtain - | ⟨h₁, h₂, h₃⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
eb b_1 : Ordinal.{0}
h : e.NFBelow eb
h_1 : a.NFBelow e.repr
h₃ : e.repr < b_1
a_ih : e.repr < ω ^ eb
IH : a.repr < ω ^ e.repr
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ b_1
have oadd' : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ b_1
Tactic: apply (add_lt_add_right IH _).trans_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
eb b_1 : Ordinal.{0}
h : e.NFBelow eb
h_1 : a.NFBelow e.repr
h₃ : e.repr < b_1
a_ih : e.repr < ω ^ eb
IH : a.repr < ω ^ e.repr
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ b_1
have h₁ : 0 < ω
Tactic: grw [← mul_succ, succ_le_of_lt (natCast_lt_omega0 _), ← opow_succ, succ_le_of_lt h₃]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
b : Ordinal.{0}
h : o.NFBelow b
⊢ o.repr < ω ^ b
have zero : ∀ {b : Ordinal.{0}}, repr 0 < ω ^ b
Tactic: induction h with
  | zero => exact opow_pos _ omega0_pos
  | oadd' _ _ h₃ _ IH =>
    rw [repr]
    apply (add_lt_add_right IH _).trans_le
    grw [← mul_succ, succ_le_of_lt (natCast_lt_omega0 _), ← opow_succ, succ_le_of_lt h₃]
    exact omega0_pos
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
b : Ordinal.{0}
h : o.NFBelow b
zero : ∀ {b : Ordinal.{0}}, repr 0 < ω ^ b
⊢ o.repr < ω ^ b
have oadd' : ∀ {e : ONote} {n : ℕ+} {a : ONote} {eb b : Ordinal.{0}},
  e.NFBelow eb →
    a.NFBelow e.repr → ∀ (h₃ : e.repr < b), e.repr < ω ^ eb → ∀ (IH : a.repr < ω ^ e.repr), (e.oadd n a).repr < ω ^ b
Tactic: induction h with
  | zero => exact opow_pos _ omega0_pos
  | oadd' _ _ h₃ _ IH =>
    rw [repr]
    apply (add_lt_add_right IH _).trans_le
    grw [← mul_succ, succ_le_of_lt (natCast_lt_omega0 _), ← opow_succ, succ_le_of_lt h₃]
    exact omega0_pos
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
b₁ b₂ : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
eb b : Ordinal.{0}
h₁ : e.NFBelow eb
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
a_ih : ∀ (bb : eb ≤ b₂), e.NFBelow b₂
a_ih_1 : ∀ (bb : e.repr ≤ b₂), a.NFBelow b₂
bb : b ≤ b₂
oadd' : e.NFBelow eb
oadd'₁ : a.NFBelow e.repr
⊢ (e.oadd n a).NFBelow b₂
have oadd'₂ : e.repr < b₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
b₁ b₂ : Ordinal.{0}
bb : b₁ ≤ b₂
h : o.NFBelow b₁
⊢ o.NFBelow b₂
have zero : ∀ {b : Ordinal.{0}} (bb : b ≤ b₂), NFBelow 0 b₂
Tactic: induction h with
  | zero => exact zero
  | oadd' h₁ h₂ h₃ _ _ => constructor; exacts [h₁, h₂, lt_of_lt_of_le h₃ bb]
Cleared hypotheses: bb, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
b₁ b₂ : Ordinal.{0}
bb : b₁ ≤ b₂
h : o.NFBelow b₁
zero : ∀ {b : Ordinal.{0}} (bb : b ≤ b₂), NFBelow 0 b₂
⊢ o.NFBelow b₂
have oadd' : ∀ {e : ONote} {n : ℕ+} {a : ONote} {eb b : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b),
  (∀ (bb : eb ≤ b₂), e.NFBelow b₂) → (∀ (bb : e.repr ≤ b₂), a.NFBelow b₂) → ∀ (bb : b ≤ b₂), (e.oadd n a).NFBelow b₂
Tactic: induction h with
  | zero => exact zero
  | oadd' h₁ h₂ h₃ _ _ => constructor; exacts [h₁, h₂, lt_of_lt_of_le h₃ bb]
Cleared hypotheses: bb, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' : Ordinal.{0}
h : (e.oadd n a).NFBelow b'
⊢ (e.oadd n a).NFBelow b
have oadd' : ∀ {eb : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b'), (e.oadd n a).NFBelow b
Tactic: obtain - | ⟨h₁, h₂, h₃⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
have refine : ω ^ e.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})
Tactic: refine (add_lt_add_right h₁.snd'.repr_lt _).trans_le (le_trans ?_ le_self_add)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : (↑n₁ : ℕ) < (↑n₂ : ℕ)
⊢ ω ^ e.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})
have rwa : ω ^ e.repr * succ (↑(↑n₁ : ℕ) : Ordinal.{0}) ≤ ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})
Tactic: rwa [← mul_succ, mul_le_mul_iff_right₀ (opow_pos _ omega0_pos), succ_le_iff, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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})
⊢ ω ^ e.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})
have rwa₁ : LE.le (α := Ordinal.{0}) (succ (↑(↑n₁ : ℕ) : Ordinal.{0})) (↑(↑n₂ : ℕ) : Ordinal.{0})
Tactic: rwa [← mul_succ, mul_le_mul_iff_right₀ (opow_pos _ omega0_pos), succ_le_iff, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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})
⊢ ω ^ e.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})
have rwa₂ : LT.lt (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑(↑n₂ : ℕ) : Ordinal.{0})
Tactic: rwa [← mul_succ, mul_le_mul_iff_right₀ (opow_pos _ omega0_pos), succ_le_iff, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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₂).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)
have IHe : (e₁.cmp e₂).Compares e₁ e₂
Tactic: have IHe := @cmp_compares _ _ h₁.fst h₂.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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₂
⊢ ((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)
have 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
Tactic: simp only [Ordering.Compares, gt_iff_lt] at IHe
Cleared hypotheses: IHe
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ ((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)
have 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)
Tactic: revert IHe
Cleared hypotheses: IHe
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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),
    ((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)
have 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)
Tactic: cases cmp e₁ e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ ∀
    (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)
have 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)
Tactic: cases cmp e₁ e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ ∀
    (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)
have 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)
Tactic: cases cmp e₁ e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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₂
⊢ (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)
have 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)
Tactic: subst IHe
Cleared hypotheses: e₂, h_1, h₂, IHe
-- 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
⊢ (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)
have 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)
Tactic: cases nh : cmpUsing (· < ·) (n₁ : ℕ) n₂
-- 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
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)
⊢ (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)
have 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)
Tactic: cases nh : cmpUsing (· < ·) (n₁ : ℕ) n₂
-- 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
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)
⊢ (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)
have 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)
Tactic: cases nh : cmpUsing (· < ·) (n₁ : ℕ) n₂
-- 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 : 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)
have nh₁ : (↑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
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 : 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)
have nh₁ : (↑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
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 : 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)
have nh₁ : (↑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
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.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)
have 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)
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.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)
⊢ (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₁ : ℕ) ∧ (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: 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₁ : ℕ) ∧ (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)
have nh₁ : (↑n₂ : ℕ) ≤ (↑n₁ : ℕ) ∧
  ((↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.gt = Ordering.lt ∨ ¬(↑n₂ : ℕ) < (↑n₁ : ℕ) ∧ Ordering.eq = Ordering.lt)
Tactic: rw [ite_eq_iff] at nh
Cleared hypotheses: nh