awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
        (a : α) → Ordinal.{u})
      i <
    o
have cons : i ≤ a
Tactic: suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ i ≤ a
have cons : b ≤ a
Tactic: cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
cons : b ≤ a
⊢ i ≤ a
have cons₁ : ∀ (hi : Mem i bs), i ≤ a
Tactic: cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
m : List α
o : Ordinal.{u}
hm : m.SortedGT
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m (a :: as)
⊢ ∀ i ∈ m,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
have cons : ∀ (hm : SortedGT.{u} (α := α) []) (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) [] (a :: as)) (i : α),
  Membership.mem (γ := List α) [] i →
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
Tactic: cases m with
    | nil => intro i hi; simp at hi
    | cons b bs =>
      intro i hi
      suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
      cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))
Cleared hypotheses: m, hm, hmltl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
m : List α
o : Ordinal.{u}
hm : m.SortedGT
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m (a :: as)
cons :
  ∀ (hm : SortedGT.{u} (α := α) []) (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) [] (a :: as)) (i : α),
    Membership.mem (γ := List α) [] i →
      (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          i <
        o
⊢ ∀ i ∈ m,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
have cons₁ : ∀ (b : α) (bs : List α) (hm : (b :: bs).SortedGT) (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)),
  ∀ i ∈ b :: bs,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
Tactic: cases m with
    | nil => intro i hi; simp at hi
    | cons b bs =>
      intro i hi
      suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
      cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))
Cleared hypotheses: m, hm, hmltl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
l m : List α
o : Ordinal.{u}
hl : l.SortedGT
hm : m.SortedGT
hlt :
  ∀ i ∈ l,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m l
⊢ ∀ i ∈ m,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
have nil : ∀ (hl : SortedGT.{u} (α := α) [])
  (hlt :
    ∀ (i : α),
      Membership.mem (γ := List α) [] i →
        (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
                (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
              (a : α) → Ordinal.{u})
            i <
          o)
  (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m []),
  ∀ i ∈ m,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
Tactic: cases l with
  | nil => simp at hmltl
  | cons a as =>
    cases m with
    | nil => intro i hi; simp at hi
    | cons b bs =>
      intro i hi
      suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
      cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))
Cleared hypotheses: l, hl, hlt, hmltl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
l m : List α
o : Ordinal.{u}
hl : l.SortedGT
hm : m.SortedGT
hlt :
  ∀ i ∈ l,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m l
nil :
  ∀ (hl : SortedGT.{u} (α := α) [])
    (hlt :
      ∀ (i : α),
        Membership.mem (γ := List α) [] i →
          (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
                  (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
                (a : α) → Ordinal.{u})
              i <
            o)
    (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m []),
    ∀ i ∈ m,
      (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          i <
        o
⊢ ∀ i ∈ m,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
have cons : ∀ (a : α) (as : List α) (hl : (a :: as).SortedGT)
  (hlt :
    ∀ i ∈ a :: as,
      (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          i <
        o)
  (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m (a :: as)),
  ∀ i ∈ m,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
Tactic: cases l with
  | nil => simp at hmltl
  | cons a as =>
    cases m with
    | nil => intro i hi; simp at hi
    | cons b bs =>
      intro i hi
      suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
      cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))
Cleared hypotheses: l, hl, hlt, hmltl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H 0 = H0
have rw : (if h : Eq.{u_2 + 2} (α := Ordinal.{u_2}) 0 0 then Eq.rec (motive := fun (x : Ordinal.{u_2}) (h : 0 = x) ↦ C x) H0 sorry
  else H 0 h (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (0 % b ^ log b 0))) =
  H0
Tactic: rw [CNF.rec, dif_pos rfl]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
rw :
  (if h : Eq.{u_2 + 2} (α := Ordinal.{u_2}) 0 0 then Eq.rec (motive := fun (x : Ordinal.{u_2}) (h : 0 = x) ↦ C x) H0 ⋯
    else H 0 h (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (0 % b ^ log b 0))) =
    H0
⊢ CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H 0 = H0
have rw₁ : Eq.rec (motive := fun (x : Ordinal.{u_2}) (h : 0 = x) ↦ C x) H0 sorry = H0
Tactic: rw [CNF.rec, dif_pos rfl]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H o = H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
have rw : (if h : o = 0 then Eq.rec (motive := fun (x : Ordinal.{u_2}) (h : 0 = x) ↦ C x) H0 sorry
  else H o h (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (o % b ^ log b o))) =
  H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
Tactic: rw [CNF.rec, dif_neg]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
rw :
  (if h : o = 0 then Eq.rec (motive := fun (x : Ordinal.{u_2}) (h : 0 = x) ↦ C x) H0 ⋯
    else H o h (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (o % b ^ log b o))) =
    H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
⊢ CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H o = H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
have rw₁ : H o ho (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (o % b ^ log b o)) =
  H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
Tactic: rw [CNF.rec, dif_neg]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
rw :
  (if h : o = 0 then Eq.rec (motive := fun (x : Ordinal.{u_2}) (h : 0 = x) ↦ C x) H0 ⋯
    else H o h (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (o % b ^ log b o))) =
    H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
rw₁ :
  H o ho (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (o % b ^ log b o)) =
    H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
⊢ CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H o = H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
have hnc : ¬o = 0
Tactic: rw [CNF.rec, dif_neg]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (hypothesis)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ CNF b (b ^ e * x + y) = (e, x) :: CNF b y
have hb' : b ≠ ⊥
Tactic: have hb' := hb.ne_bot
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
⊢ CNF b (b ^ e * x + y) = (e, x) :: CNF b y
have rw : (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
    CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
  (e, x) :: CNF b y
Tactic: rw [CNF.ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
⊢ CNF b (b ^ e * x + y) = (e, x) :: CNF b y
have rw₁ : b ^ e * x + y ≠ 0
Tactic: rw [CNF.ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
have rw : (e + log b x, (b ^ e * x + y) / b ^ (e + log b x)) :: CNF b ((b ^ e * x + y) % b ^ (e + log b x)) = (e, x) :: CNF b y
Tactic: rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (e + log b x, (b ^ e * x + y) / b ^ (e + log b x)) :: CNF b ((b ^ e * x + y) % b ^ (e + log b x)) = (e, x) :: CNF b y
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
have rw₁ : (e + 0, (b ^ e * x + y) / b ^ (e + 0)) :: CNF b ((b ^ e * x + y) % b ^ (e + 0)) = (e, x) :: CNF b y
Tactic: rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (e + log b x, (b ^ e * x + y) / b ^ (e + log b x)) :: CNF b ((b ^ e * x + y) % b ^ (e + log b x)) = (e, x) :: CNF b y
rw₁ : (e + 0, (b ^ e * x + y) / b ^ (e + 0)) :: CNF b ((b ^ e * x + y) % b ^ (e + 0)) = (e, x) :: CNF b y
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
have rw₂ : (e, (b ^ e * x + y) / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
Tactic: rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (e + log b x, (b ^ e * x + y) / b ^ (e + log b x)) :: CNF b ((b ^ e * x + y) % b ^ (e + log b x)) = (e, x) :: CNF b y
rw₁ : (e + 0, (b ^ e * x + y) / b ^ (e + 0)) :: CNF b ((b ^ e * x + y) % b ^ (e + 0)) = (e, x) :: CNF b y
rw₂ : (e, (b ^ e * x + y) / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
have rw₃ : (e, x + y / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
Tactic: rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (e + log b x, (b ^ e * x + y) / b ^ (e + log b x)) :: CNF b ((b ^ e * x + y) % b ^ (e + log b x)) = (e, x) :: CNF b y
rw₁ : (e + 0, (b ^ e * x + y) / b ^ (e + 0)) :: CNF b ((b ^ e * x + y) % b ^ (e + 0)) = (e, x) :: CNF b y
rw₂ : (e, (b ^ e * x + y) / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₃ : (e, x + y / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
have rw₄ : (e, x + 0) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
Tactic: rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (e + log b x, (b ^ e * x + y) / b ^ (e + log b x)) :: CNF b ((b ^ e * x + y) % b ^ (e + log b x)) = (e, x) :: CNF b y
rw₁ : (e + 0, (b ^ e * x + y) / b ^ (e + 0)) :: CNF b ((b ^ e * x + y) % b ^ (e + 0)) = (e, x) :: CNF b y
rw₂ : (e, (b ^ e * x + y) / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₃ : (e, x + y / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₄ : (e, x + 0) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
have rw₅ : (e, x) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
Tactic: rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (e + log b x, (b ^ e * x + y) / b ^ (e + log b x)) :: CNF b ((b ^ e * x + y) % b ^ (e + log b x)) = (e, x) :: CNF b y
rw₁ : (e + 0, (b ^ e * x + y) / b ^ (e + 0)) :: CNF b ((b ^ e * x + y) % b ^ (e + 0)) = (e, x) :: CNF b y
rw₂ : (e, (b ^ e * x + y) / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₃ : (e, x + y / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₄ : (e, x + 0) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₅ : (e, x) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
have rw₆ : (e, x) :: CNF b (y % b ^ e) = (e, x) :: CNF b y
Tactic: rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (e + log b x, (b ^ e * x + y) / b ^ (e + log b x)) :: CNF b ((b ^ e * x + y) % b ^ (e + log b x)) = (e, x) :: CNF b y
rw₁ : (e + 0, (b ^ e * x + y) / b ^ (e + 0)) :: CNF b ((b ^ e * x + y) % b ^ (e + 0)) = (e, x) :: CNF b y
rw₂ : (e, (b ^ e * x + y) / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₃ : (e, x + y / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₄ : (e, x + 0) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₅ : (e, x) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₆ : (e, x) :: CNF b (y % b ^ e) = (e, x) :: CNF b y
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
have rw₇ : (e, x) :: CNF b y = (e, x) :: CNF b y
Tactic: rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
hb : b ≤ 1
ho : o ≠ 0
⊢ CNF b o = [(0, o)]
have inl : ∀ (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1), CNF 0 o = [(0, o)]
Tactic: rcases Order.le_one_iff.1 hb with (rfl | rfl)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
hb : b ≤ 1
ho : o ≠ 0
inl : ∀ (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1), CNF 0 o = [(0, o)]
⊢ CNF b o = [(0, o)]
have inr : ∀ (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1), CNF 1 o = [(0, o)]
Tactic: rcases Order.le_one_iff.1 hb with (rfl | rfl)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ CNF b o = [(0, o)]
have rw : (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) = [(0, o)]
Tactic: rw [CNF.ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, zero_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
rw : (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) = [(0, o)]
⊢ CNF b o = [(0, o)]
have rw₁ : (0, o / HPow.hPow (β := Ordinal.{u_1}) b 0) :: CNF b (o % HPow.hPow (β := Ordinal.{u_1}) b 0) = [(0, o)]
Tactic: rw [CNF.ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, zero_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
rw : (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) = [(0, o)]
rw₁ : (0, o / HPow.hPow (β := Ordinal.{u_1}) b 0) :: CNF b (o % HPow.hPow (β := Ordinal.{u_1}) b 0) = [(0, o)]
⊢ CNF b o = [(0, o)]
have rw₂ : (0, o / 1) :: CNF b (o % 1) = [(0, o)]
Tactic: rw [CNF.ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, zero_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
rw : (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) = [(0, o)]
rw₁ : (0, o / HPow.hPow (β := Ordinal.{u_1}) b 0) :: CNF b (o % HPow.hPow (β := Ordinal.{u_1}) b 0) = [(0, o)]
rw₂ : (0, o / 1) :: CNF b (o % 1) = [(0, o)]
⊢ CNF b o = [(0, o)]
have rw₃ : (0, o) :: CNF b (o % 1) = [(0, o)]
Tactic: rw [CNF.ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, zero_right]