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₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1
⊢ (e₁.oadd n.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
have eq : ω ^ e₁.repr * (↑(succ n) : Ordinal.{0}) + a₁.repr =
  ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr - (ω ^ e₁.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)
Tactic: simp only [Nat.succPNat, Nat.succ_eq_add_one, repr, PNat.mk_coe, ← succ_eq_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1
⊢ ω ^ e₁.repr * (↑(succ n) : Ordinal.{0}) + a₁.repr =
    ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr - (ω ^ e₁.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)
have eq : ω ^ e₁.repr * (↑(succ n) : Ordinal.{0}) + a₁.repr = ω ^ e₁.repr * (↑(n + 1) : Ordinal.{0}) + a₁.repr - a₂.repr
Tactic: rw [(tsub_eq_iff_eq_add_of_le <| le_of_lt <| Nat.lt_of_sub_eq_succ mn).1 mn, add_comm,
          Nat.cast_add, mul_add, add_assoc, add_sub_add_cancel]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this_1 : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n : ℕ
mn : (↑n₁ : ℕ) - (↑n₂ : ℕ) = n + 1
⊢ ω ^ e₁.repr * (↑(succ n) : Ordinal.{0}) + a₁.repr = ω ^ e₁.repr * (↑(n + 1) : Ordinal.{0}) + a₁.repr - a₂.repr
have eq : ω ^ e₁.repr ≤ ω ^ e₁.repr * (↑(succ n) : Ordinal.{0})
Tactic: refine
          (Ordinal.sub_eq_of_add_eq <|
              add_of_omega0_opow_le h₂.snd'.repr_lt <| le_trans ?_ le_self_add).symm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
⊢ 0 * o = 0
have zero : 0 * zero = 0
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
zero : 0 * ONote.zero = 0
⊢ 0 * o = 0
have oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote), 0 * a.oadd a_1 a_2 = 0
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
⊢ o * 0 = 0
have zero : zero * 0 = 0
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
zero : ONote.zero * 0 = 0
⊢ o * 0 = 0
have oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote), a.oadd a_1 a_2 * 0 = 0
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
have IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
Tactic: have IH := oadd_mul_nfBelow h₁ h₂.snd
-- 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₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
have pos : ∀ (e0 : e₂ = 0), (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
Tactic: by_cases e0 : e₂ = 0
-- 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₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
pos : ∀ (e0 : e₂ = 0), (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
have neg : ∀ (e0 : ¬e₂ = 0), (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
Tactic: by_cases e0 : e₂ = 0
-- 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₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
have pos : (e₁.oadd (n₁ * n₂) a₁).NFBelow (e₁.repr + b₂)
Tactic: simp only [e0, oadd_mul, ↓reduceIte]
-- 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₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
have neg : ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
Tactic: simp only [e0, oadd_mul, ↓reduceIte]
-- 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₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ (e₁.oadd (n₁ * n₂) a₁).NFBelow (e₁.repr + b₂)
have pos : e₁.repr < e₁.repr + b₂
Tactic: apply NFBelow.oadd h₁.fst h₁.snd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
⊢ ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
have this : e₁.NF
Tactic: haveI := h₁.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this : e₁.NF
⊢ ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
have this₁ : e₂.NF
Tactic: haveI := h₂.fst
-- 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₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
⊢ ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
have neg : (e₁ + e₂).NF
Tactic: apply NFBelow.oadd
-- 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₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
neg : (e₁ + e₂).NF
⊢ ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
have neg₁ : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁ + e₂).repr
Tactic: apply NFBelow.oadd
-- 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₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
neg : (e₁ + e₂).NF
neg₁ : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁ + e₂).repr
⊢ ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
have neg₂ : (e₁ + e₂).repr < e₁.repr + b₂
Tactic: apply NFBelow.oadd
-- 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₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
⊢ (e₁ + e₂).repr < e₁.repr + b₂
have neg : e₂.repr < b₂
Tactic: rw [repr_add, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
h : NF 0
h₂ : o.NF
⊢ (0 * o).NF
have zero : ∀ (h₂ : zero.NF), (0 * zero).NF
Tactic: cases o
Cleared hypotheses: o, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
h : NF 0
h₂ : o.NF
zero : ∀ (h₂ : ONote.zero.NF), (0 * ONote.zero).NF
⊢ (0 * o).NF
have oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote) (h₂ : (a.oadd a_1 a_2).NF), (0 * a.oadd a_1 a_2).NF
Tactic: cases o
Cleared hypotheses: o, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
h : NF 0
h₂ : o.NF
⊢ (0 * o).repr = repr 0 * o.repr
have zero : ∀ (h₂ : zero.NF), (0 * zero).repr = repr 0 * zero.repr
Tactic: cases o
Cleared hypotheses: o, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
h : NF 0
h₂ : o.NF
zero : ∀ (h₂ : ONote.zero.NF), (0 * ONote.zero).repr = repr 0 * ONote.zero.repr
⊢ (0 * o).repr = repr 0 * o.repr
have oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote) (h₂ : (a.oadd a_1 a_2).NF),
  (0 * a.oadd a_1 a_2).repr = repr 0 * (a.oadd a_1 a_2).repr
Tactic: cases o
Cleared hypotheses: o, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
have IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
Tactic: have IH : repr (mul _ _) = _ := @repr_mul _ _ h₁ h₂.snd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
| (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
have lhs : (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr
Tactic: lhs
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
| (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
have simp : (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr
Tactic: lhs
      simp [(· * ·)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
⊢ a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
have apply : ω ^ e₁.repr ≤ ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
Tactic: apply add_of_omega0_opow_le h₁.snd'.repr_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
have ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
Tactic: have ao : repr a₁ + ω ^ repr e₁ * (n₁ : ℕ) = ω ^ repr e₁ * (n₁ : ℕ) := by
      apply add_of_omega0_opow_le h₁.snd'.repr_lt
      simpa using (mul_le_mul_iff_right₀ <| opow_pos _ omega0_pos).2 (Nat.cast_le.2 n₁.2)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
have pos : ∀ (e0 : e₂ = 0), (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
Tactic: by_cases e0 : e₂ = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
pos : ∀ (e0 : e₂ = 0), (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
have neg : ∀ (e0 : ¬e₂ = 0), (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
Tactic: by_cases e0 : e₂ = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : e₂ = 0
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
have pos : ∀ (x : ℕ) (xe : (↑n₂ : ℕ) = x.succ),
  (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
Tactic: obtain ⟨x, xe⟩ := Nat.exists_eq_succ_of_ne_zero n₂.ne_zero
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : e₂ = 0
x : ℕ
xe : (↑n₂ : ℕ) = x.succ
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
have pos : ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₁.repr =
  (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ((↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)
Tactic: simp only [Mul.mul, mul, e0, ↓reduceIte, repr, PNat.mul_coe, natCast_mul, opow_zero, one_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : e₂ = 0
x : ℕ
xe : (↑n₂ : ℕ) = x.succ
⊢ ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ((↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)
have pos : ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑x.succ : Ordinal.{0}) + a₁.repr =
  (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (↑x.succ : Ordinal.{0})
Tactic: simp only [xe, h₂.zero_of_zero e0, repr, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : e₂ = 0
x : ℕ
xe : (↑n₂ : ℕ) = x.succ
⊢ ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑x.succ : Ordinal.{0}) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (↑x.succ : Ordinal.{0})
have pos : ω ^ e₁.repr * ((↑(↑n₁ : ℕ) : Ordinal.{0}) * HAdd.hAdd (α := Ordinal.{0}) (↑x : Ordinal.{0}) 1) + a₁.repr =
  (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * HAdd.hAdd (α := Ordinal.{0}) (↑x : Ordinal.{0}) 1
Tactic: rw [Nat.cast_add_one x, ← succ_eq_add_one, add_mul_succ _ ao, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : e₂ = 0
x : ℕ
xe : (↑n₂ : ℕ) = x.succ
pos :
  ω ^ e₁.repr * ((↑(↑n₁ : ℕ) : Ordinal.{0}) * HAdd.hAdd (α := Ordinal.{0}) (↑x : Ordinal.{0}) 1) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * HAdd.hAdd (α := Ordinal.{0}) (↑x : Ordinal.{0}) 1
⊢ ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑x.succ : Ordinal.{0}) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (↑x.succ : Ordinal.{0})
have pos₁ : ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (succ (↑x : Ordinal.{0})) + a₁.repr =
  (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * succ (↑x : Ordinal.{0})
Tactic: rw [Nat.cast_add_one x, ← succ_eq_add_one, add_mul_succ _ ao, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : e₂ = 0
x : ℕ
xe : (↑n₂ : ℕ) = x.succ
pos :
  ω ^ e₁.repr * ((↑(↑n₁ : ℕ) : Ordinal.{0}) * HAdd.hAdd (α := Ordinal.{0}) (↑x : Ordinal.{0}) 1) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * HAdd.hAdd (α := Ordinal.{0}) (↑x : Ordinal.{0}) 1
pos₁ :
  ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (succ (↑x : Ordinal.{0})) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * succ (↑x : Ordinal.{0})
⊢ ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑x.succ : Ordinal.{0}) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (↑x.succ : Ordinal.{0})
have pos₂ : ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (succ (↑x : Ordinal.{0})) + a₁.repr =
  ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) * succ (↑x : Ordinal.{0}) + a₁.repr
Tactic: rw [Nat.cast_add_one x, ← succ_eq_add_one, add_mul_succ _ ao, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : e₂ = 0
x : ℕ
xe : (↑n₂ : ℕ) = x.succ
pos :
  ω ^ e₁.repr * ((↑(↑n₁ : ℕ) : Ordinal.{0}) * HAdd.hAdd (α := Ordinal.{0}) (↑x : Ordinal.{0}) 1) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * HAdd.hAdd (α := Ordinal.{0}) (↑x : Ordinal.{0}) 1
pos₁ :
  ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (succ (↑x : Ordinal.{0})) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * succ (↑x : Ordinal.{0})
pos₂ :
  ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (succ (↑x : Ordinal.{0})) + a₁.repr =
    ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) * succ (↑x : Ordinal.{0}) + a₁.repr
⊢ ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑x.succ : Ordinal.{0}) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (↑x.succ : Ordinal.{0})
have pos₃ : ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (succ (↑x : Ordinal.{0})) + a₁.repr =
  ω ^ e₁.repr * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (succ (↑x : Ordinal.{0})) + a₁.repr
Tactic: rw [Nat.cast_add_one x, ← succ_eq_add_one, add_mul_succ _ ao, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : ¬e₂ = 0
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)
have this : e₁.NF
Tactic: haveI := h₁.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : ¬e₂ = 0
this : e₁.NF
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)
have this₁ : e₂.NF
Tactic: haveI := h₂.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)
have neg : ω ^ e₁.repr * ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) +
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * a₂.repr =
  (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})) +
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * a₂.repr
Tactic: simp only [Mul.mul, mul, e0, ite_false, repr.eq_2, repr_add, opow_add, IH, repr, mul_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
⊢ ω ^ e₁.repr * ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) +
      (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * a₂.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0})) +
      (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * a₂.repr
have neg : ω ^ e₁.repr * ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) +
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * a₂.repr =
  (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) +
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * a₂.repr
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
e0 : ¬e₂ = 0
this_1 : e₁.NF
this : e₂.NF
⊢ ω ^ e₁.repr * ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) +
      (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * a₂.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ω ^ e₂.repr * (↑(↑n₂ : ℕ) : Ordinal.{0}) +
      (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * a₂.repr
have neg : ω ^ e₁.repr * ω ^ e₂.repr = (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ω ^ e₂.repr
Tactic: congr 2