awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
⊢ repr
      (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
have oadd : ∀ (e₂ : o₂.split' = (b', 0)) (r₂ : o₂.repr = ω * b'.repr + (↑0 : Ordinal.{0})),
  repr
      (match (motive := ONote × ℕ → ONote) (scale 1 b', 0) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
Tactic: rcases k with - | k
Cleared hypotheses: k, e₂, r₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
k : ℕ
e₂ : o₂.split' = (b', k)
left : b'.NF
r₂ : o₂.repr = ω * b'.repr + (↑k : Ordinal.{0})
oadd :
  ∀ (e₂ : o₂.split' = (b', 0)) (r₂ : o₂.repr = ω * b'.repr + (↑0 : Ordinal.{0})),
    repr
        (match (motive := ONote × ℕ → ONote) (scale 1 b', 0) with
        | (b, 0) => (a0 * b).oadd 1 0
        | (b, k.succ) =>
          (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
      (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
⊢ repr
      (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
have oadd₁ : ∀ (k : ℕ) (e₂ : o₂.split' = (b', k + 1)) (r₂ : o₂.repr = ω * b'.repr + (↑(k + 1) : Ordinal.{0})),
  repr
      (match (motive := ONote × ℕ → ONote) (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
Tactic: rcases k with - | k
Cleared hypotheses: k, e₂, r₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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})
⊢ repr
      (match (motive := ONote × ℕ → ONote) (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m) =
    (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ o₂.repr
have oadd : ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
    ((a0 * scale 1 b').opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
  ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ ω) ^ b'.repr *
    ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
      (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))
Tactic: simp [r₂, opow_add, opow_mul, mul_assoc, add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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})
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
      ((a0 * scale 1 b').opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))
have oadd : ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
    ω ^ (a0 * scale 1 b').repr * (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
  ((ω ^ a0.repr) ^ ω) ^ b'.repr *
    ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
      (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))
Tactic: rw [repr_opow_aux₁ a00 al aa, scale_opowAux]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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})
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
      ω ^ (a0 * scale 1 b').repr * (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))
have oadd : ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
    ((ω ^ a0.repr) ^ ω) ^ b'.repr * (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
  ((ω ^ a0.repr) ^ ω) ^ b'.repr *
    ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
      (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))
Tactic: simp only [repr_mul, repr_scale, repr, opow_zero, PNat.val_ofNat, Nat.cast_one, mul_one,
        add_zero, opow_one, opow_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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})
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr)) +
      ((ω ^ a0.repr) ^ ω) ^ b'.repr * (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + (a'.repr + (↑m : Ordinal.{0}))))
have oadd : ((ω ^ a0.repr) ^ ω) ^ b'.repr *
    ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
      (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr) =
  ((ω ^ a0.repr) ^ ω) ^ b'.repr *
    ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ k *
      (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})))
Tactic: rw [← mul_add, ← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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})
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr) +
        (opowAux 0 a0 (a0.oadd n a' * (↑m : ONote)) k m).repr) =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})) ^ k *
        (ω ^ a0.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a'.repr + (↑m : Ordinal.{0})))
have oadd : (ω ^ 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: congr 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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})
⊢ (ω ^ 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}))
have 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})
Tactic: rw [← pow_succ, ← opow_natCast, ← opow_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ ∃ (i : α), a < b + f i
have inl : ∀ (h : a < b), ∃ (i : α), a < b + f i
Tactic: rcases lt_or_ge a b with h | h'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ ∃ (i : α), a < b + f i
have inr : ∀ (h' : b ≤ a), ∃ (i : α), a < b + f i
Tactic: rcases lt_or_ge a b with h | h'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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 : α), a < b + f i
have inl : ∀ (i : α), ∃ (i : α), a < b + f i
Tactic: obtain ⟨i⟩ := id hα
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
have h₁ : a - b < o
Tactic: rw [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
have inr : ∀ (i : α) (H : a - b < f i), a < b + f i
Tactic: refine (H h).imp fun i H => ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ a < b + f i
have inr : b + (a - b) < b + f i
Tactic: rwa [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o a : Ordinal.{u_1}
h : a < o * ω
⊢ ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o
have obtain : ∀ (i : Ordinal.{u_1}) (hi : i < ω) (h' : a < o * i), ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o
Tactic: obtain ⟨i, hi, h'⟩ := (lt_mul_iff_of_isSuccLimit isSuccLimit_omega0).1 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o a : Ordinal.{u_1}
h : a < o * ω
i : Ordinal.{u_1}
hi : i < ω
h' : a < o * i
⊢ ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o
have obtain : ∀ (i : ℕ) (hi : (↑i : Ordinal.{u_1}) < ω) (h' : a < o * (↑i : Ordinal.{u_1})),
  ∃ (i : ℕ), a < o * (↑i : Ordinal.{u_1}) + o
Tactic: obtain ⟨i, rfl⟩ := lt_omega0.1 hi
Cleared hypotheses: i, hi, h'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ ∃ (i : α), a < b ^ f i
have obtain : ∀ (d : Ordinal.{u_2}) (hd : d < o) (h' : a < b ^ d), ∃ (i : α), a < b ^ f i
Tactic: obtain ⟨d, hd, h'⟩ := (lt_opow_of_isSuccLimit (zero_lt_one.trans hb).ne' ho).1 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o : ONote
⊢ o.FundamentalSequenceProp o.fundamentalSequence
have 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
Tactic: induction o with
  | zero => exact rfl
  | oadd a m b iha ihb
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
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
have 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))
Tactic: rw [fundamentalSequence]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
⊢ (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))
have oadd : ∀ (e : b.fundamentalSequence = Sum.inl none),
  (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: rcases e : b.fundamentalSequence with (⟨_ | b'⟩ | f)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
oadd :
  ∀ (e : b.fundamentalSequence = Sum.inl none),
    (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))
⊢ (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))
have oadd₁ : ∀ (b' : ONote) (e : b.fundamentalSequence = Sum.inl (some b')),
  (a.oadd m b).FundamentalSequenceProp
    (match (motive := Option ONote ⊕ (ℕ → ONote) → Option ONote ⊕ (ℕ → ONote)) Sum.inl (some b') 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: rcases e : b.fundamentalSequence with (⟨_ | b'⟩ | f)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
e : b.fundamentalSequence = Sum.inl none
⊢ (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))
have 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
Tactic: simp only [FundamentalSequenceProp]