awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
⊢ ω ∣ o'.repr
have rcases : ∀ (a : ONote) (n : ℕ) (e : o.split' = (a, n)), ω ∣ o'.repr
Tactic: rcases e : split' o with ⟨a, n⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ ω ∣ o'.repr
have h₁ : (scale 1 a, n) = (o', m)
Tactic: rw [split_eq_scale_split' e] at h
Cleared hypotheses: h, e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o o' : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
⊢ ω ∣ o'.repr
have fst_eq : scale 1 a = o'
Tactic: injection h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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'
⊢ ω ∣ o'.repr
have snd_eq : n = m
Tactic: injection h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ ω ∣ o'.repr
have subst : ω ∣ (scale 1 a).repr
Tactic: subst o'
Cleared hypotheses: o', fst_eq
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq : n = m
⊢ ω ∣ (scale 1 a).repr
have left : a.NF
Tactic: cases nf_repr_split' e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o : ONote
m : ℕ
inst : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq : n = m
left : a.NF
⊢ ω ∣ (scale 1 a).repr
have right : o.repr = ω * a.repr + (↑n : Ordinal.{0})
Tactic: cases nf_repr_split' e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst : o.NF
h : o.split = (e.oadd n a, m)
⊢ a.repr + (↑m : Ordinal.{0}) < ω ^ e.repr
have h₁ : (e.oadd n a).NF
Tactic: obtain ⟨h₁, h₂⟩ := nf_repr_split h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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
⊢ a.repr + (↑m : Ordinal.{0}) < ω ^ e.repr
have h₂ : o.repr = (e.oadd n a).repr + (↑m : Ordinal.{0})
Tactic: obtain ⟨h₁, h₂⟩ := nf_repr_split h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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})
⊢ a.repr + (↑m : Ordinal.{0}) < ω ^ e.repr
have e0 : e.repr ≠ 0
Tactic: obtain ⟨e0, d⟩ := h₁.of_dvd_omega0 (split_dvd h)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
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 + (↑m : Ordinal.{0}) < ω ^ e.repr
have d : ω ∣ a.repr
Tactic: obtain ⟨e0, d⟩ := h₁.of_dvd_omega0 (split_dvd h)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ a.repr + (↑m : Ordinal.{0}) < ω ^ e.repr
have apply : ω ≤ ω ^ e.repr
Tactic: apply isPrincipal_add_omega0_opow _ h₁.snd'.repr_lt (lt_of_lt_of_le (natCast_lt_omega0 _) _)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
n : ℕ
o : ONote
⊢ o.mulNat n = o * (↑n : ONote)
have zero : zero.mulNat n = zero * (↑n : ONote)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
n : ℕ
o : ONote
zero : ONote.zero.mulNat n = ONote.zero * (↑n : ONote)
⊢ o.mulNat n = o * (↑n : ONote)
have oadd : ∀ (a : ONote) (a_1 : ℕ+) (a_2 : ONote), (a.oadd a_1 a_2).mulNat n = a.oadd a_1 a_2 * (↑n : ONote)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
n : ℕ
⊢ zero.mulNat n = zero * (↑n : ONote)
have zero : zero.mulNat 0 = zero * (↑0 : ONote)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
n : ℕ
zero : ONote.zero.mulNat 0 = ONote.zero * (↑0 : ONote)
⊢ ONote.zero.mulNat n = ONote.zero * (↑n : ONote)
have zero₁ : ∀ (n : ℕ), ONote.zero.mulNat (n + 1) = ONote.zero * (↑(n + 1) : ONote)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
n : ℕ
a : ONote
a_1 : ℕ+
a_2 : ONote
⊢ (a.oadd a_1 a_2).mulNat n = a.oadd a_1 a_2 * (↑n : ONote)
have oadd : (a.oadd a_1 a_2).mulNat 0 = a.oadd a_1 a_2 * (↑0 : ONote)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ (a.oadd a_1 a_2).mulNat n = a.oadd a_1 a_2 * (↑n : ONote)
have oadd₁ : ∀ (n : ℕ), (a.oadd a_1 a_2).mulNat (n + 1) = a.oadd a_1 a_2 * (↑(n + 1) : ONote)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
⊢ (e.opowAux a0 a k m).NF
have 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)
Tactic: unfold opowAux
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k : ℕ
⊢ 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)
have 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)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ 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)
have 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)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
m 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)
have this : ∀ (m : ℕ), (e.opowAux a0 a k m).NF
Tactic: haveI := nf_opowAux e a0 a k
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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
⊢ 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)
have succ : ((e + a0 * (↑k : ONote)).scale a + e.opowAux a0 a k m.succ).NF
Tactic: simp only [mulNat_eq_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
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)
have 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)
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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
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)
⊢ 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)
have 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)
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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
⊢ 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)
have zero : 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 m with
  | zero => cases k <;> exact NF.zero
  | succ m =>
    cases k with
    | zero => exact NF.oadd_zero _ _
    | succ k =>
      haveI := nf_opowAux e a0 a k
      simp only [mulNat_eq_mul]; infer_instance
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
e a0 a : ONote
inst : e.NF
inst_1 : a0.NF
inst_2 : a.NF
k m : ℕ
zero :
  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)
⊢ 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)
have succ : ∀ (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 m with
  | zero => cases k <;> exact NF.zero
  | succ m =>
    cases k with
    | zero => exact NF.oadd_zero _ _
    | succ k =>
      haveI := nf_opowAux e a0 a k
      simp only [mulNat_eq_mul]; infer_instance
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
⊢ (o₁ ^ o₂).NF
have rcases : ∀ (a : ONote) (m : ℕ) (e₁ : o₁.split = (a, m)), (o₁ ^ o₂).NF
Tactic: rcases e₁ : split o₁ with ⟨a, m⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
⊢ (o₁ ^ o₂).NF
have na : a.NF
Tactic: have na := (nf_repr_split e₁).1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
⊢ (o₁ ^ o₂).NF
have rcases : ∀ (b' : ONote) (k : ℕ) (e₂ : o₂.split' = (b', k)), (o₁ ^ o₂).NF
Tactic: rcases e₂ : split' o₂ with ⟨b', k⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ (o₁ ^ o₂).NF
have this : b'.NF
Tactic: haveI := (nf_repr_split' e₂).1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
⊢ (o₁ ^ o₂).NF
have zero : ∀ (e₁ : o₁.split = (zero, m)) (na : zero.NF), (o₁ ^ o₂).NF
Tactic: obtain - | ⟨a0, n, a'⟩ := a
Cleared hypotheses: a, e₁, na
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
zero : ∀ (e₁ : o₁.split = (ONote.zero, m)) (na : ONote.zero.NF), (o₁ ^ o₂).NF
⊢ (o₁ ^ o₂).NF
have oadd : ∀ (a0 : ONote) (n : ℕ+) (a' : ONote) (e₁ : o₁.split = (a0.oadd n a', m)) (na : (a0.oadd n a').NF), (o₁ ^ o₂).NF
Tactic: obtain - | ⟨a0, n, a'⟩ := a
Cleared hypotheses: a, e₁, na
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
e₁ : o₁.split = (zero, m)
na : zero.NF
⊢ (o₁ ^ o₂).NF
have zero : ∀ (e₁ : o₁.split = (zero, 0)), (o₁ ^ o₂).NF
Tactic: rcases m with - | m
Cleared hypotheses: m, e₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
e₁ : o₁.split = (ONote.zero, m)
na : ONote.zero.NF
zero : ∀ (e₁ : o₁.split = (ONote.zero, 0)), (o₁ ^ o₂).NF
⊢ (o₁ ^ o₂).NF
have zero₁ : ∀ (m : ℕ) (e₁ : o₁.split = (ONote.zero, m + 1)), (o₁ ^ o₂).NF
Tactic: rcases m with - | m
Cleared hypotheses: m, e₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
⊢ (o₁ ^ o₂).NF
have pos : o₂ = 0 → (o₁ ^ o₂).NF
Tactic: by_cases o₂ = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
pos : o₂ = 0 → (o₁ ^ o₂).NF
⊢ (o₁ ^ o₂).NF
have neg : ¬o₂ = 0 → (o₁ ^ o₂).NF
Tactic: by_cases o₂ = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : o₂ = 0
⊢ (o₁ ^ o₂).NF
have pos : NF (if True then 1 else 0)
Tactic: simp only [(· ^ ·), Pow.pow, opow, opowAux2, *]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).NF
have neg : NF (if False then 1 else 0)
Tactic: simp only [(· ^ ·), Pow.pow, opow, opowAux2, *]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
⊢ (o₁ ^ o₂).NF
have pos : m = 0 → (o₁ ^ o₂).NF
Tactic: by_cases m = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
pos : m = 0 → (o₁ ^ o₂).NF
⊢ (o₁ ^ o₂).NF
have neg : ¬m = 0 → (o₁ ^ o₂).NF
Tactic: by_cases m = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : m = 0
⊢ (o₁ ^ o₂).NF
have pos : NF 1
Tactic: simp only [(· ^ ·), Pow.pow, opow, opowAux2, *, zero_def]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : ¬m = 0
⊢ (o₁ ^ o₂).NF
have neg : (b'.oadd (Monoid.npow k m.succPNat) 0).NF
Tactic: simp only [(· ^ ·), Pow.pow, opow, opowAux2, *]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
⊢ (o₁ ^ o₂).NF
have oadd : NF
  (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
  | (b, 0) => (a0 * b).oadd 1 0
  | (b, k.succ) =>
    (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
Tactic: simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, split_eq_scale_split' e₂, mulNat_eq_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (hypothesis)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
have this₁ : a0.NF
Tactic: have := na.fst
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
have oadd : ∀ (e₂ : o₂.split' = (b', 0)),
  NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', 0) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
Tactic: rcases k with - | k
Cleared hypotheses: k, e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
oadd :
  ∀ (e₂ : o₂.split' = (b', 0)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', 0) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
have oadd₁ : ∀ (k : ℕ) (e₂ : o₂.split' = (b', k + 1)),
  NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
Tactic: rcases k with - | k
Cleared hypotheses: k, e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
have oadd : ∀ (e₂ : o₂.split' = (b', HAdd.hAdd (α := ℕ) 0 1)),
  NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
Tactic: cases k
Cleared hypotheses: k, e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
oadd :
  ∀ (e₂ : o₂.split' = (b', HAdd.hAdd (α := ℕ) 0 1)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', k + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
have oadd₁ : ∀ (n_1 : ℕ) (e₂ : o₂.split' = (b', n_1 + 1 + 1)),
  NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', n_1 + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
Tactic: cases k
Cleared hypotheses: k, e₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', HAdd.hAdd (α := ℕ) 0 1)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
have oadd : ∀ (e₁ : o₁.split = (a0.oadd n a', 0)),
  NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑0 : ONote)) k 0)
Tactic: cases m
Cleared hypotheses: m, e₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Notation (goal)
Goal:
o₁ o₂ : ONote
inst : o₁.NF
inst_1 : o₂.NF
m : ℕ
b' : ONote
this_1 : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', HAdd.hAdd (α := ℕ) 0 1)
oadd :
  ∀ (e₁ : o₁.split = (a0.oadd n a', 0)),
    NF
      (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑0 : ONote)) k 0)
⊢ NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * (↑m : ONote)) k m)
have oadd₁ : ∀ (n_1 : ℕ) (e₁ : o₁.split = (a0.oadd n a', n_1 + 1)),
  NF
    (match (motive := ONote × ℕ → ONote) (scale 1 b', HAdd.hAdd (α := ℕ) 0 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * (↑k : ONote)).scale (a0.oadd n a') +
        (a0 * b).opowAux a0 (a0.oadd n a' * (↑(n_1 + 1) : ONote)) k (n_1 + 1))
Tactic: cases m
Cleared hypotheses: m, e₁