awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
left : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})
oadd :
  HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
      (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
      (↑(k + 1) : Ordinal.{0})
⊢ (ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
      (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ k *
      (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))

Tactic:
rw [← pow_succ, ← opow_natCast, ← opow_natCast]

Premises used: pow_succ, Ordinal.opow_natCast
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
left : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})
⊢ HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
      (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
      (↑(k + 1) : Ordinal.{0})

Tactic:
(repr_opow_aux₂ _ ad a00 al _ _).2

Premises used: Order.succ, And.right, ONote.repr_opow_aux₂, Nat.unaryCast
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + (↑m : Ordinal.{0})
this_1 : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + (↑m : Ordinal.{0}) < ω ^ a0.repr
aa : (a' + (↑m : ONote)).repr = a'.repr + (↑m : Ordinal.{0})
b' : ONote
left : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})
⊢ HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr) (↑k : Ordinal.{0}) * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
      (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    HPow.hPow (β := Ordinal.{0}) (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0}))
      (↑(k + 1) : Ordinal.{0})

Tactic:
exact (repr_opow_aux₂ _ ad a00 al _ _).2

Premises used: And.right, ONote.repr_opow_aux₂
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
b a : Ordinal.{u_2}
h : a < b + o
inl : ∀ (h : a < b), ∃ (i : α), a < b + f i
inr : ∀ (h' : b ≤ a), ∃ (i : α), a < b + f i
⊢ ∃ (i : α), a < b + f i

Tactic:
rcases lt_or_ge a b with h | h'

Premises used: lt_or_ge
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
b a : Ordinal.{u_2}
h_1 : a < b + o
h : a < b
inl : ∀ (i : α), ∃ (i : α), a < b + f i
⊢ ∃ (i : α), a < b + f i

Tactic:
obtain ⟨i⟩ := id hα

Premises used: id
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
b a : Ordinal.{u_2}
h_1 : a < b + o
h : a < b
i : α
⊢ ∃ (i : α), a < b + f i

Tactic:
⟨i, h.trans_le le_self_add⟩

Premises used: LT.lt.trans_le, Exists.intro, le_self_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
b a : Ordinal.{u_2}
h_1 : a < b + o
h : a < b
i : α
⊢ ∃ (i : α), a < b + f i

Tactic:
exact ⟨i, h.trans_le le_self_add⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
b a : Ordinal.{u_2}
h : a < b + o
h' : b ≤ a
⊢ a - b < o

Tactic:
rw [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left] at h

Premises used: Ordinal.add_sub_cancel_of_le, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
b a : Ordinal.{u_2}
h : a < b + o
h' : b ≤ a
h₁ : a - b < o
⊢ b ≤ a

Tactic:
rw [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left] at h

Premises used: Ordinal.add_sub_cancel_of_le, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
⊢ ∃ (i : α), a < b + f i

Tactic:
(H h).imp fun i H => ?_

Premises used: Exists.imp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
inr : ∀ (i : α) (H : a - b < f i), a < b + f i
⊢ ∃ (i : α), a < b + f i

Tactic:
refine (H h).imp fun i H => ?_

Premises used: Exists.imp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H_1 : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
i : α
H : a - b < f i
inr : b + (a - b) < b + f i
inr₁ inr₂ inr₃ inr₄ : a - b < f i
⊢ a < b + f i

Tactic:
rwa [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left]

Premises used: Ordinal.add_sub_cancel_of_le, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o a : Ordinal.{u_1}
h : a < o * ω
obtain : ∀ (i : Ordinal.{u_1}) (hi : i < ω) (h' : a < o * i), ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o
⊢ ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o

Tactic:
obtain ⟨i, hi, h'⟩ := (lt_mul_iff_of_isSuccLimit isSuccLimit_omega0).1 h

Premises used: Ordinal.isSuccLimit_omega0, Iff.mp, Ordinal.lt_mul_iff_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o a : Ordinal.{u_1}
h : a < o * ω
i : Ordinal.{u_1}
hi : i < ω
h' : a < o * i
obtain :
  ∀ (i : ℕ) (hi : (↑i : Ordinal.{u_1}) < ω) (h' : a < o * (↑i : Ordinal.{u_1})),
    ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o
⊢ ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o

Tactic:
obtain ⟨i, rfl⟩ := lt_omega0.1 hi

Premises used: Iff.mp, Ordinal.lt_omega0, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o a : Ordinal.{u_1}
h : a < o * ω
i : ℕ
hi : (↑i : Ordinal.{u_1}) < ω
h' : a < o * (↑i : Ordinal.{u_1})
⊢ ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o

Tactic:
⟨i, h'.trans_le le_self_add⟩

Premises used: LT.lt.trans_le, Exists.intro, le_self_add
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o a : Ordinal.{u_1}
h : a < o * ω
i : ℕ
hi : (↑i : Ordinal.{u_1}) < ω
h' : a < o * (↑i : Ordinal.{u_1})
⊢ ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o

Tactic:
exact ⟨i, h'.trans_le le_self_add⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
o b : Ordinal.{u_2}
hb : 1 < b
ho : IsSuccLimit o
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
a : Ordinal.{u_2}
h : a < b ^ o
obtain : ∀ (d : Ordinal.{u_2}) (hd : d < o) (h' : a < b ^ d), ∃ (i : α), a < b ^ f i
⊢ ∃ (i : α), a < b ^ f i

Tactic:
obtain ⟨d, hd, h'⟩ := (lt_opow_of_isSuccLimit (zero_lt_one.trans hb).ne' ho).1 h

Premises used: LT.lt.ne', zero_lt_one, Iff.mp, LT.lt.trans, Ordinal.lt_opow_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
o b : Ordinal.{u_2}
hb : 1 < b
ho : IsSuccLimit o
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
a : Ordinal.{u_2}
h : a < b ^ o
d : Ordinal.{u_2}
hd : d < o
h' : a < b ^ d
⊢ ∃ (i : α), a < b ^ f i

Tactic:
(H hd).imp fun i hi => h'.trans <| (opow_lt_opow_iff_right hb).2 hi

Premises used: Iff.mpr, Exists.imp, LT.lt.trans, Ordinal.opow_lt_opow_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
α : Sort u_1
o b : Ordinal.{u_2}
hb : 1 < b
ho : IsSuccLimit o
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ (i : α), a < f i
a : Ordinal.{u_2}
h : a < b ^ o
d : Ordinal.{u_2}
hd : d < o
h' : a < b ^ d
⊢ ∃ (i : α), a < b ^ f i

Tactic:
exact (H hd).imp fun i hi => h'.trans <| (opow_lt_opow_iff_right hb).2 hi

Premises used: Iff.mpr, Exists.imp, LT.lt.trans, Ordinal.opow_lt_opow_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
⊢ o.FundamentalSequenceProp (Sum.inl none) ↔ o = 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o a : ONote
⊢ o.FundamentalSequenceProp (Sum.inl (some a)) ↔ o.repr = succ a.repr ∧ (o.NF → a.NF)

Tactic:
Iff.rfl

Premises used: Iff.rfl, ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
f : ℕ → ONote
⊢ o.FundamentalSequenceProp (Sum.inr f) ↔
    IsSuccLimit o.repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < o ∧ (o.NF → (f i).NF)) ∧ ∀ a < o.repr, ∃ (i : ℕ), a < (f i).repr

Tactic:
Iff.rfl

Premises used: Iff.rfl, ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ zero.FundamentalSequenceProp zero.fundamentalSequence

Tactic:
rfl

Premises used: ONote.FundamentalSequenceProp, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ zero.FundamentalSequenceProp zero.fundamentalSequence

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
oadd :
  ∀ (a : ONote) (m : ℕ+) (b : ONote) (iha : a.FundamentalSequenceProp a.fundamentalSequence)
    (ihb : b.FundamentalSequenceProp b.fundamentalSequence),
    (a.oadd m b).FundamentalSequenceProp (a.oadd m b).fundamentalSequence
⊢ o.FundamentalSequenceProp o.fundamentalSequence

Tactic:
induction o with
  | zero => exact rfl
  | oadd a m b iha ihb

Premises used: ONote.oadd, ONote.zero, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
oadd :
  (a.oadd m b).FundamentalSequenceProp
    (match (motive := Option ONote ⊕ (ℕ → ONote) → Option ONote ⊕ (ℕ → ONote)) b.fundamentalSequence with
    | Sum.inr f => Sum.inr fun (i : ℕ) ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) a.fundamentalSequence,
        m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero))
⊢ (a.oadd m b).FundamentalSequenceProp (a.oadd m b).fundamentalSequence

Tactic:
rw [fundamentalSequence]

Premises used: ONote.fundamentalSequence
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
e : b.fundamentalSequence = Sum.inl none
oadd :
  match (motive := Option ONote ⊕ (ℕ → ONote) → Prop)
    match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) a.fundamentalSequence, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (f i).repr
⊢ (a.oadd m b).FundamentalSequenceProp
    (match (motive := Option ONote ⊕ (ℕ → ONote) → Option ONote ⊕ (ℕ → ONote)) Sum.inl none with
    | Sum.inr f => Sum.inr fun (i : ℕ) ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match (motive := Option ONote ⊕ (ℕ → ONote) → ℕ → Option ONote ⊕ (ℕ → ONote)) a.fundamentalSequence,
        m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun (i : ℕ) ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun (i : ℕ) ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun (i : ℕ) ↦ a.oadd m.succPNat ((f i).oadd 1 zero))

Tactic:
simp only [FundamentalSequenceProp]

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
e : b.fundamentalSequence = Sum.inl none
⊢ b = 0

Tactic:
rw [e, FundamentalSequenceProp] at ihb

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
e : b.fundamentalSequence = Sum.inl none
ihb₁ : b = 0
⊢ b.fundamentalSequence = Sum.inl none

Tactic:
rw [e, FundamentalSequenceProp] at ihb

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
b' : ONote
e : b.fundamentalSequence = Sum.inl (some b')
⊢ b.repr = succ b'.repr ∧ (b.NF → b'.NF)

Tactic:
rw [e, FundamentalSequenceProp] at ihb

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
b' : ONote
e : b.fundamentalSequence = Sum.inl (some b')
ihb₁ : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
⊢ b.fundamentalSequence = Sum.inl (some b')

Tactic:
rw [e, FundamentalSequenceProp] at ihb

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
⊢ IsSuccLimit b.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ (i : ℕ), a < (f i).repr

Tactic:
rw [e, FundamentalSequenceProp] at ihb

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
ihb₁ :
  IsSuccLimit b.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ (i : ℕ), a < (f i).repr
⊢ b.fundamentalSequence = Sum.inr f

Tactic:
rw [e, FundamentalSequenceProp] at ihb

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ a = 0

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
iha₁ : a = 0
⊢ b = 0

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
iha₁ : a = 0
ihb₁ : b = 0
⊢ b.fundamentalSequence = Sum.inl none

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
iha₁ : a = 0
ihb₁ : b = 0
e₁ : b.fundamentalSequence = Sum.inl none
⊢ a.fundamentalSequence = Sum.inl none

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
iha₁ : a = 0
ihb₁ : b = 0
e₁ : b.fundamentalSequence = Sum.inl none
e₂ : a.fundamentalSequence = Sum.inl none
⊢ m.natPred = 0

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
oadd :
  ∀ (iha : a = 0) (ihb : b = 0) (e : b.fundamentalSequence = Sum.inl none) (e : a.fundamentalSequence = Sum.inl none)
    (m' : ℕ) (e' : m.natPred = m' + 1),
    (a.oadd m b).repr = succ (zero.oadd m'.succPNat zero).repr ∧ ((a.oadd m b).NF → (zero.oadd m'.succPNat zero).NF)
⊢ (a.oadd m b).repr = succ (zero.oadd m'.succPNat zero).repr ∧ ((a.oadd m b).NF → (zero.oadd m'.succPNat zero).NF)

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
⊢ a.repr = succ a'.repr ∧ (a.NF → a'.NF)

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
iha₁ : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
⊢ a.fundamentalSequence = Sum.inl (some a')

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
iha₁ : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e₁ : a.fundamentalSequence = Sum.inl (some a')
⊢ m.natPred = 0

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
a' : ONote
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
oadd :
  ∀ (iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)) (e : a.fundamentalSequence = Sum.inl (some a')) (m' : ℕ)
    (e' : m.natPred = m' + 1),
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ),
          a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m'.succPNat (a'.oadd (i + 1).succPNat zero) ∧
            a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m b ∧
              ((a.oadd m b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m'.succPNat (a'.oadd (i + 1).succPNat zero) ∧
          a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ (i : ℕ), a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
iha₁ :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
⊢ a.fundamentalSequence = Sum.inr f

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e_1 : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
iha₁ :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ (i : ℕ), a_1 < (f i).repr
e₁ : a.fundamentalSequence = Sum.inr f
⊢ m.natPred = 0

Tactic:
rw [e, FundamentalSequenceProp] at iha

Premises used: ONote.FundamentalSequenceProp