awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∀ (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.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)
Tactic: cases cmp a₁ a₂
-- 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
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)
⊢ ∀ (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.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)
Tactic: cases cmp a₁ a₂
-- 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₁ = 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)
have 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)
Tactic: subst IHa
Cleared hypotheses: a₂, h, h₂, IHa
-- 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
case case₁ :
  ∀
    (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)
case₂ case₃ :
  ∀ (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)
⊢ ∀
    (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)
have case₄ : ∀ (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: case eq =>
      intro IHe; dsimp at IHe; subst IHe
      unfold _root_.cmp; cases nh : cmpUsing (· < ·) (n₁ : ℕ) n₂ <;>
      rw [cmpUsing, ite_eq_iff, not_lt] at nh
      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
      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
      rcases nh with nh | nh
      · cases nh; contradiction
      obtain ⟨nhl, nhr⟩ := nh
      rw [ite_eq_iff] at nhr
      rcases nhr with nhr | nhr
      · cases nhr; contradiction
      obtain rfl := Subtype.ext (nhl.eq_of_not_lt nhr.1)
      have IHa := @cmp_compares _ _ h₁.snd h₂.snd
      revert IHa; cases cmp a₁ a₂ <;> intro IHa <;> dsimp at IHa
      case lt => exact oadd_lt_oadd_3 IHa
      case gt => exact oadd_lt_oadd_3 IHa
      subst IHa; exact rfl
Cleared hypotheses: e₂, h_1, h₂
-- 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
case case₁ :
  ∀
    (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)
case₂ case₃ :
  ∀ (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)
case₄ :
  ∀ (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)
⊢ ∀
    (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)
have case₅ : ∀ (h_2 : o₂ = e₁.oadd n₂ a₂) (h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h_2).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_2)
Tactic: case eq =>
      intro IHe; dsimp at IHe; subst IHe
      unfold _root_.cmp; cases nh : cmpUsing (· < ·) (n₁ : ℕ) n₂ <;>
      rw [cmpUsing, ite_eq_iff, not_lt] at nh
      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
      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
      rcases nh with nh | nh
      · cases nh; contradiction
      obtain ⟨nhl, nhr⟩ := nh
      rw [ite_eq_iff] at nhr
      rcases nhr with nhr | nhr
      · cases nhr; contradiction
      obtain rfl := Subtype.ext (nhl.eq_of_not_lt nhr.1)
      have IHa := @cmp_compares _ _ h₁.snd h₂.snd
      revert IHa; cases cmp a₁ a₂ <;> intro IHa <;> dsimp at IHa
      case lt => exact oadd_lt_oadd_3 IHa
      case gt => exact oadd_lt_oadd_3 IHa
      subst IHa; exact rfl
Cleared hypotheses: e₂, h_1, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr
have this : ¬(e.oadd n a).repr = repr 0
Tactic: have := mt repr_inj.1 (fun h => by injection h : ONote.oadd e n a ≠ 0)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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 ∧ ω ^ b ∣ a.repr
have L : 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)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ ω ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ ω ∣ a.repr
have rw : HPow.hPow (β := Ordinal.{0}) ω 1 ∣ (e.oadd n a).repr → 1 ≤ e.repr ∧ HPow.hPow (β := Ordinal.{0}) ω 1 ∣ a.repr
Tactic: rw [← opow_one ω, ← one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b o : ONote
⊢ Decidable (b.TopBelow o)
have zero : Decidable (b.TopBelow zero)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b o : ONote
zero : Decidable (b.TopBelow ONote.zero)
⊢ Decidable (b.TopBelow o)
have oadd : (a : ONote) → (a_1 : ℕ+) → (a_2 : ONote) → Decidable (b.TopBelow (a.oadd a_1 a_2))
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
⊢ Decidable (e.oadd n a).NF
have have : (this : Decidable e.NF) → Decidable (e.oadd n a).NF
Tactic: have := decidableNF e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
this : Decidable e.NF
⊢ Decidable (e.oadd n a).NF
have have : (this : Decidable a.NF) → Decidable (e.oadd n a).NF
Tactic: have := decidableNF a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
this_1 : Decidable e.NF
this : Decidable a.NF
⊢ Decidable (e.oadd n a).NF
have h : e.NF ∧ a.NF ∧ e.TopBelow a ↔ (e.oadd n a).NF
Tactic: apply decidable_of_iff (NF e ∧ NF a ∧ TopBelow e a)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a : ONote
this_1 : Decidable e.NF
this : Decidable a.NF
⊢ e.NF ∧ a.NF ∧ e.TopBelow a ↔ (e.oadd n a).NF
have h : e.NF ∧ a.NFBelow e.repr ↔ (e.oadd n a).NF
Tactic: rw [← and_congr_right fun h => @nfBelow_iff_topBelow _ h _]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (e.oadd n a + o).NFBelow b
have h' : (a + o).NFBelow b
Tactic: have h' := add_nfBelow (h₁.snd.mono <| le_of_lt h₁.lt) h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.oadd n a + o).NFBelow b
have simp : (e.addAux n (a + o)).NFBelow b
Tactic: simp only [oadd_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.addAux n (a + o)).NFBelow b
have revert : ∀ (h' : (a + o).NFBelow b), (e.addAux n (a + o)).NFBelow b
Tactic: revert h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ ∀ (h' : (a + o).NFBelow b), (e.addAux n (a + o)).NFBelow b
have zero : ∀ (h' : zero.NFBelow b), (e.addAux n zero).NFBelow b
Tactic: obtain - | ⟨e', n', a'⟩ := a + o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
zero : ∀ (h' : ONote.zero.NFBelow b), (e.addAux n ONote.zero).NFBelow b
⊢ ∀ (h' : (a + o).NFBelow b), (e.addAux n (a + o)).NFBelow b
have oadd : ∀ (e' : ONote) (n' : ℕ+) (a' : ONote) (h' : (e'.oadd n' a').NFBelow b), (e.addAux n (e'.oadd n' a')).NFBelow b
Tactic: obtain - | ⟨e', n', a'⟩ := a + o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b
have this : (e.cmp e').Compares e e'
Tactic: have : ((e.cmp e').Compares e e') := @cmp_compares _ _ h₁.fst h'.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b
have oadd : ∀ (h : e.cmp e' = Ordering.lt), (e.addAux n (e'.oadd n' a')).NFBelow b
Tactic: cases h : cmp e e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
oadd : ∀ (h : e.cmp e' = Ordering.lt), (e.addAux n (e'.oadd n' a')).NFBelow b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b
have oadd₁ : ∀ (h : e.cmp e' = Ordering.eq), (e.addAux n (e'.oadd n' a')).NFBelow b
Tactic: cases h : cmp e e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
oadd : ∀ (h : e.cmp e' = Ordering.lt), (e.addAux n (e'.oadd n' a')).NFBelow b
oadd₁ : ∀ (h : e.cmp e' = Ordering.eq), (e.addAux n (e'.oadd n' a')).NFBelow b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b
have oadd₂ : ∀ (h : e.cmp e' = Ordering.gt), (e.addAux n (e'.oadd n' a')).NFBelow b
Tactic: cases h : cmp e e'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b
have oadd : NFBelow
  (match (motive := Ordering → ONote) e.cmp e' with
  | Ordering.lt => e'.oadd n' a'
  | Ordering.eq => e.oadd (n + n') a'
  | Ordering.gt => e.oadd n (e'.oadd n' a'))
  b
Tactic: dsimp [addAux]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b
have oadd : NFBelow
  (match (motive := Ordering → ONote) e.cmp e' with
  | Ordering.lt => e'.oadd n' a'
  | Ordering.eq => e.oadd (n + n') a'
  | Ordering.gt => e.oadd n (e'.oadd n' a'))
  b
Tactic: dsimp [addAux]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b
have oadd : NFBelow
  (match (motive := Ordering → ONote) e.cmp e' with
  | Ordering.lt => e'.oadd n' a'
  | Ordering.eq => e.oadd (n + n') a'
  | Ordering.gt => e.oadd n (e'.oadd n' a'))
  b
Tactic: dsimp [addAux]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ NFBelow
    (match (motive := Ordering → ONote) e.cmp e' with
    | Ordering.lt => e'.oadd n' a'
    | Ordering.eq => e.oadd (n + n') a'
    | Ordering.gt => e.oadd n (e'.oadd n' a'))
    b
have oadd : (e.oadd (n + n') a').NFBelow b
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ NFBelow
    (match (motive := Ordering → ONote) e.cmp e' with
    | Ordering.lt => e'.oadd n' a'
    | Ordering.eq => e.oadd (n + n') a'
    | Ordering.gt => e.oadd n (e'.oadd n' a'))
    b
have oadd : (e.oadd n (e'.oadd n' a')).NFBelow b
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b
have this₁ : Ordering.eq.Compares e e'
Tactic: simp only [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.eq
this : Ordering.eq.Compares e e'
⊢ (e.oadd (n + n') a').NFBelow b
have h'₁ : (e.oadd n' a').NFBelow b
Tactic: subst e'
Cleared hypotheses: e', h', h, this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.eq
this : Ordering.eq.Compares e e'
h'₁ : (e.oadd n' a').NFBelow b
⊢ (e.oadd (n + n') a').NFBelow b
have h₃ : e.cmp e = Ordering.eq
Tactic: subst e'
Cleared hypotheses: e', h', h, this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b
have this₁ : Ordering.gt.Compares e e'
Tactic: simp only [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
have this : a.NF
Tactic: haveI := h₁.snd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
have h' : (a + o).repr = a.repr + o.repr
Tactic: have h' := repr_add a o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a + o).repr = a.repr + o.repr
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
have h'₁ : (a.add o).repr = a.repr + o.repr
Tactic: conv_lhs at h' => simp [HAdd.hAdd, Add.add]
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
have nf : (a + o).NF
Tactic: have nf := ONote.add_nf a o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a + o).NF
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
have nf₁ : (a.add o).NF
Tactic: conv at nf => simp [HAdd.hAdd, Add.add]
Cleared hypotheses: nf
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a.add o).NF
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
have zero : ∀ (h : a.add o = zero), ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
Tactic: rcases h : add a o with - | ⟨e', n', a'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a.add o).NF
zero : ∀ (h : a.add o = ONote.zero), ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
have oadd : ∀ (e' : ONote) (n' : ℕ+) (a' : ONote) (h : a.add o = e'.oadd n' a'),
  ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
Tactic: rcases h : add a o with - | ⟨e', n', a'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a.add o).NF
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
⊢ ((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
have oadd : ∀ (nf : (e'.oadd n' a').NF),
  repr
      (match (motive := Ordering → ONote) e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
Tactic: simp only [add, addAux, h'.symm, h, add_assoc, repr] at nf h₁ ⊢
Cleared hypotheses: nf
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
⊢ repr
      (match (motive := Ordering → ONote) e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have this₁ : e.NF
Tactic: have := h₁.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this : e.NF
⊢ repr
      (match (motive := Ordering → ONote) e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have this₁ : e'.NF
Tactic: haveI := nf.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this_1 : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this_2 : e.NF
this : e'.NF
⊢ repr
      (match (motive := Ordering → ONote) e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')) =
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω ^ e'.repr * (↑(↑n' : ℕ) : Ordinal.{0}) + a'.repr)
have ee : (e.cmp e').Compares e e'
Tactic: have ee := cmp_compares e e'