awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
h_1 : (e - 1).oadd n a' = o'
h_2 : m' = m
neg :
  ((e - 1).oadd n a').NF ∧
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
      ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
⊢ o'.NF ∧
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) = ω * o'.repr + (↑m : Ordinal.{0})

Tactic:
substs o' m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
⊢ ¬e.repr = repr 0

Tactic:
have := mt repr_inj.1 e0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ¬e.repr = repr 0
rw : ω ^ e.repr = ω ^ (1 + (e.repr - 1))
rw₁ rw₂ : ω ^ e.repr = ω ^ e.repr
⊢ ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)

Tactic:
rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)]

Premises used: Iff.mpr, Ordinal.opow_add, Order.one_le_iff_ne_zero, Ordinal.add_sub_cancel_of_le
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
⊢ ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)

Tactic:
have : (ω : Ordinal.{0}) ^ repr e = ω ^ (1 : Ordinal.{0}) * ω ^ (repr e - 1) := by
        have := mt repr_inj.1 e0
        rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
⊢ (e - 1).NF

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
neg : a'.NFBelow (e - 1).repr
neg₁ :
  ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
    ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
⊢ ((e - 1).oadd n a').NF ∧
    ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
      ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})

Tactic:
refine ⟨NF.oadd (by infer_instance) _ ?_, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
neg : ∀ (this : ω ^ e.repr = ω * ω ^ (e.repr - 1)), a'.NFBelow (e.repr - 1)
⊢ a'.NFBelow (e - 1).repr

Tactic:
simp only [opow_one, repr_sub, repr_one, Nat.cast_one] at this ⊢

Premises used: ONote.repr_one, Ordinal.opow_one, Nat.cast_one, ONote.repr_sub
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
⊢ a'.NFBelow (e.repr - 1)

Tactic:
IH₁.below_of_lt' <| (mul_lt_mul_iff_right₀ omega0_pos).1 <|
          (le_self_add (α := Ordinal) (b := m')).trans_lt ?_

Premises used: Ordinal.omega0_pos, ONote.NF.below_of_lt', mul_lt_mul_iff_right₀, Iff.mp, le_self_add, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
neg : ω * a'.repr + (↑m' : Ordinal.{0}) < ω * ω ^ (e.repr - 1)
⊢ a'.NFBelow (e.repr - 1)

Tactic:
refine IH₁.below_of_lt' <| (mul_lt_mul_iff_right₀ omega0_pos).1 <|
          (le_self_add (α := Ordinal) (b := m')).trans_lt ?_

Premises used: Ordinal.omega0_pos, mul_lt_mul_iff_right₀, Iff.mp, le_self_add, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
neg : a.repr < ω ^ e.repr
⊢ ω * a'.repr + (↑m' : Ordinal.{0}) < ω * ω ^ (e.repr - 1)

Tactic:
rw [← this, ← IH₂]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
⊢ a.repr < ω ^ e.repr

Tactic:
h.snd'.repr_lt

Premises used: ONote.NF.snd', ONote.NFBelow.repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
⊢ a.repr < ω ^ e.repr

Tactic:
exact h.snd'.repr_lt

Premises used: ONote.NF.snd', ONote.NFBelow.repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
neg :
  HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1) * (↑(↑n : ℕ) : Ordinal.{0}) +
      (ω * a'.repr + (↑m' : Ordinal.{0})) =
    ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) =
    ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})

Tactic:
rw [this]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this_1 : e.NF
this_2 : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + (↑m' : Ordinal.{0})
this : ω ^ e.repr = HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1)
⊢ HPow.hPow (β := Ordinal.{0}) ω 1 * ω ^ (e.repr - 1) * (↑(↑n : ℕ) : Ordinal.{0}) +
      (ω * a'.repr + (↑m' : Ordinal.{0})) =
    ω * ((e - 1).oadd n a').repr + (↑m' : Ordinal.{0})

Tactic:
simp [mul_add, mul_assoc, add_assoc]

Premises used: add_assoc, mul_assoc, mul_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ a.NF

Tactic:
haveI := h.snd
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
pos : ∀ (e0 : e = 0), (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
neg : ∀ (e0 : ¬e = 0), (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
by_cases e0 : e = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
pos : (x + e).oadd n (x.oadd 1 0 * a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
simp_rw [scale_eq_mul]
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + 0).repr = x.repr

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + e).oadd n (x.oadd 1 0 * a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
simp [Mul.mul, mul, e0, h.zero_of_zero,
        show x + 0 = x from repr_inj.1 (by simp)]

Premises used: ONote.NF.zero_of_zero, ONote.mul, ONote.repr_inj, Mul.mul, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
inst : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : ¬e = 0
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
simp [e0, Mul.mul, mul, scale_eq_mul, (· * ·)]

Premises used: ONote.mul, HMul.hMul, Mul.mul
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
inst : x.NF
o : ONote
inst_1 : o.NF
rw : (x.oadd 1 0 * o).NF
⊢ (x.scale o).NF

Tactic:
rw [scale_eq_mul]

Premises used: ONote.scale_eq_mul
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
inst : x.NF
o : ONote
inst_1 : o.NF
⊢ (x.oadd 1 0 * o).NF

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x : ONote
inst : x.NF
o : ONote
inst_1 : o.NF
⊢ (x.scale o).repr = ω ^ x.repr * o.repr

Tactic:
simp only [scale_eq_mul, repr_mul, repr, PNat.one_coe, Nat.cast_one, mul_one, add_zero]

Premises used: ONote.repr_mul, PNat.one_coe, ONote.repr, ONote.scale_eq_mul, mul_one, add_zero, Nat.cast_one
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
rcases : ∀ (a : ONote) (n : ℕ) (e : o.split' = (a, n)), o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})
⊢ o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})

Tactic:
rcases e : split' o with ⟨a, n⟩

Premises used: ONote.split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ a.NF

Tactic:
obtain ⟨s₁, s₂⟩ := nf_repr_split' e

Premises used: ONote.nf_repr_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
⊢ o.repr = ω * a.repr + (↑n : Ordinal.{0})

Tactic:
obtain ⟨s₁, s₂⟩ := nf_repr_split' e

Premises used: ONote.nf_repr_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
⊢ (scale 1 a, n) = (o', m)

Tactic:
rw [split_eq_scale_split' e] at h

Premises used: ONote.split_eq_scale_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
h₁ : (scale 1 a, n) = (o', m)
⊢ o.split' = (a, n)

Tactic:
rw [split_eq_scale_split' e] at h

Premises used: ONote.split_eq_scale_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
h₁ : (scale 1 a, n) = (o', m)
e₁ : o.split' = (a, n)
⊢ a.NF

Tactic:
rw [split_eq_scale_split' e] at h

Premises used: ONote.split_eq_scale_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
h₁ : (scale 1 a, n) = (o', m)
e₁ : o.split' = (a, n)
s₃ : a.NF
⊢ o.repr = ω * a.repr + (↑n : Ordinal.{0})

Tactic:
rw [split_eq_scale_split' e] at h

Premises used: ONote.split_eq_scale_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
⊢ scale 1 a = o'

Tactic:
injection h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
fst_eq : scale 1 a = o'
⊢ n = m

Tactic:
injection h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + (↑n : Ordinal.{0})
fst_eq : scale 1 a = o'
snd_eq : n = m
substs :
  ∀ (e : o.split' = (a, m)) (s₂ : o.repr = ω * a.repr + (↑m : Ordinal.{0})),
    (scale 1 a).NF ∧ o.repr = (scale 1 a).repr + (↑m : Ordinal.{0})
⊢ o'.NF ∧ o.repr = o'.repr + (↑m : Ordinal.{0})

Tactic:
substs o' n
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
m : ℕ
inst : o.NF
a : ONote
s₁ : a.NF
e : o.split' = (a, m)
s₂ : o.repr = ω * a.repr + (↑m : Ordinal.{0})
simp : (scale 1 a).NF
⊢ (scale 1 a).NF ∧ o.repr = (scale 1 a).repr + (↑m : Ordinal.{0})

Tactic:
simp only [repr_scale, repr_one, Nat.cast_one, opow_one, ← s₂, and_true]

Premises used: ONote.repr_one, Ordinal.opow_one, and_true, ONote.repr_scale, Nat.cast_one
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
m : ℕ
inst : o.NF
a : ONote
s₁ : a.NF
e : o.split' = (a, m)
s₂ : o.repr = ω * a.repr + (↑m : Ordinal.{0})
⊢ (scale 1 a).NF

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
rcases : ∀ (a : ONote) (n : ℕ) (e : o.split' = (a, n)), ω ∣ o'.repr
⊢ ω ∣ o'.repr

Tactic:
rcases e : split' o with ⟨a, n⟩

Premises used: ONote.split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ (scale 1 a, n) = (o', m)

Tactic:
rw [split_eq_scale_split' e] at h

Premises used: ONote.split_eq_scale_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
h₁ : (scale 1 a, n) = (o', m)
⊢ o.split' = (a, n)

Tactic:
rw [split_eq_scale_split' e] at h

Premises used: ONote.split_eq_scale_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
⊢ scale 1 a = o'

Tactic:
injection h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
fst_eq : scale 1 a = o'
⊢ n = m

Tactic:
injection h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
fst_eq : scale 1 a = o'
snd_eq : n = m
subst : ω ∣ (scale 1 a).repr
⊢ ω ∣ o'.repr

Tactic:
subst o'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq : n = m
⊢ a.NF

Tactic:
cases nf_repr_split' e

Premises used: ONote.nf_repr_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq : n = m
left : a.NF
⊢ o.repr = ω * a.repr + (↑n : Ordinal.{0})

Tactic:
cases nf_repr_split' e

Premises used: ONote.nf_repr_split'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq : n = m
left : a.NF
right : o.repr = ω * a.repr + (↑n : Ordinal.{0})
⊢ ω ∣ (scale 1 a).repr

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst : o.NF
h : o.split = (e.oadd n a, m)
⊢ (e.oadd n a).NF

Tactic:
obtain ⟨h₁, h₂⟩ := nf_repr_split h

Premises used: ONote.nf_repr_split
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
⊢ o.repr = (e.oadd n a).repr + (↑m : Ordinal.{0})

Tactic:
obtain ⟨h₁, h₂⟩ := nf_repr_split h

Premises used: ONote.nf_repr_split
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + (↑m : Ordinal.{0})
⊢ e.repr ≠ 0

Tactic:
obtain ⟨e0, d⟩ := h₁.of_dvd_omega0 (split_dvd h)

Premises used: ONote.split_dvd, ONote.NF.of_dvd_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + (↑m : Ordinal.{0})
e0 : e.repr ≠ 0
⊢ ω ∣ a.repr

Tactic:
obtain ⟨e0, d⟩ := h₁.of_dvd_omega0 (split_dvd h)

Premises used: ONote.split_dvd, ONote.NF.of_dvd_omega0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + (↑m : Ordinal.{0})
e0 : e.repr ≠ 0
d : ω ∣ a.repr
apply : ω ≤ ω ^ e.repr
⊢ a.repr + (↑m : Ordinal.{0}) < ω ^ e.repr

Tactic:
apply isPrincipal_add_omega0_opow _ h₁.snd'.repr_lt (lt_of_lt_of_le (natCast_lt_omega0 _) _)

Premises used: Ordinal.natCast_lt_omega0, Ordinal.isPrincipal_add_omega0_opow, ONote.NF.snd', lt_of_lt_of_le, ONote.NFBelow.repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + (↑m : Ordinal.{0})
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ ω ≤ ω ^ e.repr

Tactic:
simpa using opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0)

Premises used: Ordinal.opow_le_opow_right, Iff.mpr, Ordinal.omega0_pos, Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
n : ℕ
o : ONote
zero : ONote.zero.mulNat n = ONote.zero * (↑n : ONote)
oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote), (a.oadd a_1 a_2).mulNat n = a.oadd a_1 a_2 * (↑n : ONote)
⊢ o.mulNat n = o * (↑n : ONote)

Tactic:
cases o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
n : ℕ
zero : ONote.zero.mulNat 0 = ONote.zero * (↑0 : ONote)
zero₁ : ∀ (n : ℕ), ONote.zero.mulNat (n + 1) = ONote.zero * (↑(n + 1) : ONote)
⊢ ONote.zero.mulNat n = ONote.zero * (↑n : ONote)

Tactic:
cases n
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
n : ℕ
a : ONote
a_1 : ℕ+
a_2 : ONote
oadd : (a.oadd a_1 a_2).mulNat 0 = a.oadd a_1 a_2 * (↑0 : ONote)
oadd₁ : ∀ (n : ℕ), (a.oadd a_1 a_2).mulNat (n + 1) = a.oadd a_1 a_2 * (↑(n + 1) : ONote)
⊢ (a.oadd a_1 a_2).mulNat n = a.oadd a_1 a_2 * (↑n : ONote)

Tactic:
cases n
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ zero.mulNat 0 = zero * (↑0 : ONote)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
n : ℕ
⊢ zero.mulNat (n + 1) = zero * (↑(n + 1) : ONote)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
a_1 : ℕ+
a_2 : ONote
⊢ (a.oadd a_1 a_2).mulNat 0 = a.oadd a_1 a_2 * (↑0 : ONote)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
a_1 : ℕ+
a_2 : ONote
n : ℕ
⊢ (a.oadd a_1 a_2).mulNat (n + 1) = a.oadd a_1 a_2 * (↑(n + 1) : ONote)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
inst : o.NF
n : ℕ
⊢ (o.mulNat n).NF

Tactic:
simpa using ONote.mul_nf o (ofNat n)

Premises used: ONote.ofNat, ONote.mul_nf
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
unfold :
  NF
    (match (motive := ℕ → ℕ → ONote) k, m with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)
⊢ (e.opowAux a0 a k m).NF

Tactic:
unfold opowAux

Premises used: ONote.opowAux
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k : ℕ
zero :
  NF
    (match (motive := ℕ → ℕ → ONote) 0, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)
zero₁ :
  ∀ (n : ℕ),
    NF
      (match (motive := ℕ → ℕ → ONote) n + 1, 0 with
      | x, 0 => 0
      | 0, m.succ => e.oadd m.succPNat 0
      | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)
⊢ NF
    (match (motive := ℕ → ℕ → ONote) k, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
cases k
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
⊢ NF
    (match (motive := ℕ → ℕ → ONote) 0, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
NF.zero

Premises used: ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
⊢ NF
    (match (motive := ℕ → ℕ → ONote) 0, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
exact NF.zero

Premises used: ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
n : ℕ
⊢ NF
    (match (motive := ℕ → ℕ → ONote) n + 1, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
NF.zero

Premises used: ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
n : ℕ
⊢ NF
    (match (motive := ℕ → ℕ → ONote) n + 1, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
exact NF.zero

Premises used: ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
m : ℕ
⊢ NF
    (match (motive := ℕ → ℕ → ONote) 0, m + 1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
NF.oadd_zero _ _

Premises used: ONote.NF.oadd_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
m : ℕ
⊢ NF
    (match (motive := ℕ → ℕ → ONote) 0, m + 1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
exact NF.oadd_zero _ _

Premises used: ONote.NF.oadd_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
m k : ℕ
⊢ ∀ (m : ℕ), (e.opowAux a0 a k m).NF

Tactic:
haveI := nf_opowAux e a0 a k
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
m k : ℕ
this : ∀ (m : ℕ), (e.opowAux a0 a k m).NF
succ : ((e + a0 * (↑k : ONote)).scale a + e.opowAux a0 a k m.succ).NF
⊢ NF
    (match (motive := ℕ → ℕ → ONote) k + 1, m + 1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
simp only [mulNat_eq_mul]

Premises used: ONote.mulNat_eq_mul
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
m k : ℕ
this : ∀ (m : ℕ), (e.opowAux a0 a k m).NF
⊢ ((e + a0 * (↑k : ONote)).scale a + e.opowAux a0 a k m.succ).NF

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
succ :
  NF
    (match (motive := ℕ → ℕ → ONote) 0, m + 1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)
succ₁ :
  ∀ (k : ℕ),
    NF
      (match (motive := ℕ → ℕ → ONote) k + 1, m + 1 with
      | x, 0 => 0
      | 0, m.succ => e.oadd m.succPNat 0
      | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)
⊢ NF
    (match (motive := ℕ → ℕ → ONote) k, m + 1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m)

Tactic:
cases k with
    | zero => exact NF.oadd_zero _ _
    | succ k =>
      haveI := nf_opowAux e a0 a k
      simp only [mulNat_eq_mul]; infer_instance

Premises used: Order.succ, ONote.zero, ONote.NF.oadd_zero, ONote.mulNat_eq_mul