awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
simp : (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr
| (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
lhs
      simp [(· * ·)]

Premises used: HMul.hMul
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
apply : ω ^ e₁.repr ≤ ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})
⊢ a₁.repr + ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) = ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})

Tactic:
apply add_of_omega0_opow_le h₁.snd'.repr_lt

Premises used: Ordinal.add_of_omega0_opow_le, ONote.NF.snd', ONote.NFBelow.repr_lt
-- Module: Mathlib.SetTheory.Ordinal.Notation
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₁.repr ≤ ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0})

Tactic:
simpa using (mul_le_mul_iff_right₀ <| opow_pos _ omega0_pos).2 (Nat.cast_le.2 n₁.2)

Premises used: Iff.mpr, Ordinal.omega0_pos, Nat.cast_le, Ordinal.opow_pos, Subtype.property, mul_le_mul_iff_right₀
-- Module: Mathlib.SetTheory.Ordinal.Notation
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})

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)
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
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
⊢ (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
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
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
⊢ (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

Premises used: PNat.ne_zero, Nat.exists_eq_succ_of_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑(↑n₂ : ℕ) : Ordinal.{0}) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ((↑(↑n₂ : ℕ) : Ordinal.{0}) + a₂.repr)
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
simp only [Mul.mul, mul, e0, ↓reduceIte, repr, PNat.mul_coe, natCast_mul, opow_zero, one_mul]

Premises used: ONote.mul, Ordinal.natCast_mul, ONote.repr, Mul.mul, Ordinal.opow_zero, PNat.mul_coe, reduceIte, one_mul
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 * HMul.hMul (α := Ordinal.{0}) (↑(↑n₁ : ℕ) : Ordinal.{0}) (↑x.succ : Ordinal.{0}) + a₁.repr =
    (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * (↑x.succ : Ordinal.{0})
⊢ ω ^ 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 [xe, h₂.zero_of_zero e0, repr, add_zero]

Premises used: ONote.NF.zero_of_zero, ONote.repr, add_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
pos₃ 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
⊢ ω ^ 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:
rw [Nat.cast_add_one x, ← succ_eq_add_one, add_mul_succ _ ao, mul_assoc]

Premises used: Order.succ_eq_add_one, mul_assoc, Ordinal.add_mul_succ, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
⊢ e₁.NF

Tactic:
haveI := h₁.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
⊢ e₂.NF

Tactic:
haveI := h₂.fst
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
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
⊢ (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)

Tactic:
simp only [Mul.mul, mul, e0, ite_false, repr.eq_2, repr_add, opow_add, IH, repr, mul_add]

Premises used: ONote.mul, Ordinal.opow_add, ite_false, ONote.repr.eq_2, ONote.repr_add, ONote.repr, Mul.mul, mul_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
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
⊢ ω ^ 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]

Premises used: mul_assoc
-- Module: Mathlib.SetTheory.Ordinal.Notation
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
neg : ω ^ e₁.repr * ω ^ e₂.repr = (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ω ^ e₂.repr
⊢ ω ^ 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:
congr 2
-- Module: Mathlib.SetTheory.Ordinal.Notation
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 = repr 0

Tactic:
have := mt repr_inj.1 e0
-- Module: Mathlib.SetTheory.Ordinal.Notation
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_2 : e₂.NF
this : ¬e₂.repr = repr 0
neg : ω ∣ ω ^ e₂.repr
⊢ ω ^ e₁.repr * ω ^ e₂.repr = (ω ^ e₁.repr * (↑(↑n₁ : ℕ) : Ordinal.{0}) + a₁.repr) * ω ^ e₂.repr

Tactic:
rw [add_mul_of_isSuccLimit ao (isSuccLimit_opow_left isSuccLimit_omega0 this), mul_assoc,
        mul_omega0_dvd (Nat.cast_pos'.2 n₁.pos) (natCast_lt_omega0 _)]

Premises used: Iff.mpr, Ordinal.isSuccLimit_omega0, Ordinal.isSuccLimit_opow_left, mul_assoc, Ordinal.natCast_lt_omega0, PNat.pos, Ordinal.add_mul_of_isSuccLimit, Nat.cast_pos', Ordinal.mul_omega0_dvd
-- Module: Mathlib.SetTheory.Ordinal.Notation
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_2 : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ∣ ω ^ e₂.repr

Tactic:
simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 this)

Premises used: Iff.mpr, Ordinal.omega0, Ordinal.opow_dvd_opow, Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
⊢ o₁ ^ o₂ = o₂.opowAux2 o₁.split

Tactic:
rfl

Premises used: ONote.opowAux2, rfl, ONote.opow
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o' : ONote
m : ℕ
h : NF 0
p : split' 0 = (o', m)
⊢ 0 = o'

Tactic:
injection p
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o' : ONote
m : ℕ
h : NF 0
p : split' 0 = (o', m)
fst_eq : 0 = o'
⊢ 0 = m

Tactic:
injection p
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o' : ONote
m : ℕ
h : NF 0
fst_eq : 0 = o'
snd_eq : 0 = m
substs : split 0 = (scale 1 0, 0)
⊢ split 0 = (scale 1 o', m)

Tactic:
substs o' m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
⊢ split 0 = (scale 1 0, 0)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
pos : ∀ (e0 : e = 0), (e.oadd n a).split = (scale 1 o', m)
neg : ∀ (e0 : ¬e = 0), (e.oadd n a).split = (scale 1 o', m)
⊢ (e.oadd n a).split = (scale 1 o', m)

Tactic:
by_cases e0 : e = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
pos : ∀ (p : 0 = o' ∧ (↑n : ℕ) = m), 0 = scale 1 o' ∧ (↑n : ℕ) = m
⊢ (e.oadd n a).split = (scale 1 o', m)

Tactic:
simp only [split', e0, ↓reduceIte, Prod.mk.injEq, split] at p ⊢

Premises used: ONote.split', ONote.split, Prod.mk.injEq, reduceIte
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
neg : ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
⊢ (e.oadd n a).split = (scale 1 o', m)

Tactic:
simp only [split', e0, ↓reduceIte, Prod.mk.injEq, split] at p ⊢

Premises used: ONote.split', ONote.split, Prod.mk.injEq, reduceIte
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ 0 = scale 1 0 ∧ (↑n : ℕ) = (↑n : ℕ)

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ 0 = scale 1 0 ∧ (↑n : ℕ) = (↑n : ℕ)

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
neg : ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
⊢ e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
revert p
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
neg :
  ∀ (a' : ONote) (m' : ℕ) (h' : a.split' = (a', m')) (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
    e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m
⊢ ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
rcases h' : split' a with ⟨a', m'⟩

Premises used: ONote.split'
-- 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')
⊢ e.NF

Tactic:
haveI := h.fst
-- 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 : e.NF
⊢ a.NF

Tactic:
haveI := h.snd
-- 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
neg : (e - 1).oadd n a' = o' → m' = m → e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m), e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
simp only [split_eq_scale_split' h', and_imp]

Premises used: and_imp
-- 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
⊢ 1 + (e - 1) = e

Tactic:
repr_inj.1 ?_

Premises used: ONote.repr_inj, Iff.mp
-- 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
refine : (1 + (e - 1)).repr = e.repr
⊢ 1 + (e - 1) = e

Tactic:
refine repr_inj.1 ?_

Premises used: ONote.repr_inj, Iff.mp
-- 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
simp : 1 + (e.repr - 1) = e.repr
⊢ (1 + (e - 1)).repr = e.repr

Tactic:
simp only [repr_add, repr_one, Nat.cast_one, repr_sub]

Premises used: ONote.repr_one, ONote.repr_add, Nat.cast_one, ONote.repr_sub
-- 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
⊢ ¬e.repr = repr 0

Tactic:
have := mt repr_inj.1 e0
-- 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_2 : a.NF
this : ¬e.repr = repr 0
⊢ 1 + (e.repr - 1) = e.repr

Tactic:
Ordinal.add_sub_cancel_of_le <| one_le_iff_ne_zero.2 this

Premises used: Iff.mpr, Order.one_le_iff_ne_zero, Ordinal.add_sub_cancel_of_le
-- 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_2 : a.NF
this : ¬e.repr = repr 0
⊢ 1 + (e.repr - 1) = e.repr

Tactic:
exact Ordinal.add_sub_cancel_of_le <| one_le_iff_ne_zero.2 this

Premises used: Iff.mpr, Order.one_le_iff_ne_zero, Ordinal.add_sub_cancel_of_le
-- 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
⊢ 1 + (e - 1) = e

Tactic:
have : 1 + (e - 1) = e := by
        refine repr_inj.1 ?_
        simp only [repr_add, repr_one, Nat.cast_one, repr_sub]
        have := mt repr_inj.1 e0
        exact Ordinal.add_sub_cancel_of_le <| one_le_iff_ne_zero.2 this
-- 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_2 : a.NF
this : 1 + (e - 1) = e
h_1 : (e - 1).oadd n a' = o'
h_2 : m' = m
neg : e.oadd n (scale 1 a') = scale 1 ((e - 1).oadd n a') ∧ m' = m'
⊢ e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m

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_2 : a.NF
this : 1 + (e - 1) = e
⊢ e.oadd n (scale 1 a') = scale 1 ((e - 1).oadd n a') ∧ m' = m'

Tactic:
simp [scale, this]

Premises used: ONote.scale
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o' : ONote
m : ℕ
h : NF 0
fst_eq : 0 = o'
snd_eq : 0 = m
substs : NF 0 ∧ repr 0 = ω * repr 0 + (↑0 : Ordinal.{0})
⊢ o'.NF ∧ repr 0 = ω * o'.repr + (↑m : Ordinal.{0})

Tactic:
substs o' m
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
h : NF 0
⊢ NF 0 ∧ repr 0 = ω * repr 0 + (↑0 : Ordinal.{0})

Tactic:
simp [NF.zero]

Premises used: ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
pos : ∀ (e0 : e = 0), o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})
neg : ∀ (e0 : ¬e = 0), o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})

Tactic:
by_cases e0 : e = 0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
pos : ∀ (p : 0 = o' ∧ (↑n : ℕ) = m), o'.NF ∧ (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + (↑m : Ordinal.{0})

Tactic:
simp only [split', e0, ↓reduceIte, Prod.mk.injEq, repr, repr_zero, opow_zero, one_mul] at p ⊢

Premises used: ONote.split', ONote.repr_zero, ONote.repr, Prod.mk.injEq, Ordinal.opow_zero, reduceIte, one_mul
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
⊢ (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m

Tactic:
simp only [split', e0, ↓reduceIte, Prod.mk.injEq, repr, repr_zero, opow_zero, one_mul] at p ⊢

Premises used: ONote.split', ONote.repr_zero, ONote.repr, Prod.mk.injEq, Ordinal.opow_zero, reduceIte, one_mul
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : e = 0
p : 0 = o' ∧ (↑n : ℕ) = m
pos : NF 0 ∧ (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * repr 0 + (↑(↑n : ℕ) : Ordinal.{0})
⊢ o'.NF ∧ (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})

Tactic:
rcases p with ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ NF 0 ∧ (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * repr 0 + (↑(↑n : ℕ) : Ordinal.{0})

Tactic:
simp [h.zero_of_zero e0, NF.zero]

Premises used: ONote.NF.zero_of_zero, ONote.NF.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
neg :
  ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
⊢ o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})

Tactic:
revert p
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
neg :
  ∀ (a' : ONote) (m' : ℕ) (h' : a.split' = (a', m')) (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})
⊢ ∀ (p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})

Tactic:
rcases h' : split' a with ⟨a', m'⟩

Premises used: ONote.split'
-- 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
⊢ a'.NF

Tactic:
obtain ⟨IH₁, IH₂⟩ := nf_repr_split' h'
-- 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
⊢ a.repr = ω * a'.repr + (↑m' : Ordinal.{0})

Tactic:
obtain ⟨IH₁, IH₂⟩ := nf_repr_split' h'
-- 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})
neg :
  (e - 1).oadd n a' = o' →
    m' = m →
      o'.NF ∧
        ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (ω * a'.repr + (↑m' : Ordinal.{0})) = ω * o'.repr + (↑m : Ordinal.{0})
⊢ ∀ (p : (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m),
    o'.NF ∧ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr = ω * o'.repr + (↑m : Ordinal.{0})

Tactic:
simp only [IH₂, and_imp]

Premises used: and_imp