awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)]
rw₃ : (0, o) :: CNF b (o % 1) = [(0, o)]
⊢ CNF b o = [(0, o)]
have rw₄ : (0, o) :: CNF 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)]
rw₂ : (0, o / 1) :: CNF b (o % 1) = [(0, o)]
rw₃ : (0, o) :: CNF b (o % 1) = [(0, o)]
rw₄ : (0, o) :: CNF b 0 = [(0, o)]
⊢ CNF b o = [(0, o)]
have rw₅ : Eq (α := List (Ordinal.{u_1} × Ordinal.{u_1})) [(0, 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}
⊢ foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o
have refine_1 : Eq (α := Ordinal.{u_1})
  (foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b 0)) 0
Tactic: refine CNF.rec b ?_ ?_ o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
refine_1 :
  Eq (α := Ordinal.{u_1})
    (foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b 0)) 0
⊢ foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o
have refine_2 : ∀ (o : Ordinal.{u_1}),
  o ≠ 0 →
    foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0
          (CNF b (o % b ^ log b o)) =
        o % b ^ log b o →
      foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o
Tactic: refine CNF.rec b ?_ ?_ o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
⊢ Eq (α := Ordinal.{u_1})
    (foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b 0)) 0
have refine_1 : Eq.{u_1 + 2} (α := Ordinal.{u_1})
  (foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 []) 0
Tactic: rw [zero_right, foldr_nil]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
refine_1 :
  Eq.{u_1 + 2} (α := Ordinal.{u_1})
    (foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 []) 0
⊢ Eq (α := Ordinal.{u_1})
    (foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b 0)) 0
have refine_1₁ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
Tactic: rw [zero_right, foldr_nil]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH :
  foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) =
    o % b ^ log b o
⊢ foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o
have refine_2 : foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0
    ((log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)) =
  o
Tactic: rw [CNF.ne_zero ho, foldr_cons, IH, div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH :
  foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) =
    o % b ^ log b o
refine_2 :
  foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0
      ((log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)) =
    o
⊢ foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o
have refine_2₁ : b ^ (log b o, o / b ^ log b o).1 * (log b o, o / b ^ log b o).2 +
    foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0
      (CNF b (o % b ^ log b o)) =
  o
Tactic: rw [CNF.ne_zero ho, foldr_cons, IH, div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH :
  foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) =
    o % b ^ log b o
refine_2 :
  foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0
      ((log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)) =
    o
refine_2₁ :
  b ^ (log b o, o / b ^ log b o).1 * (log b o, o / b ^ log b o).2 +
      foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0
        (CNF b (o % b ^ log b o)) =
    o
⊢ foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o
have refine_2₂ : b ^ (log b o, o / b ^ log b o).1 * (log b o, o / b ^ log b o).2 + o % b ^ log b o = o
Tactic: rw [CNF.ne_zero ho, foldr_cons, IH, div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH :
  foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) =
    o % b ^ log b o
refine_2 :
  foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0
      ((log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)) =
    o
refine_2₁ :
  b ^ (log b o, o / b ^ log b o).1 * (log b o, o / b ^ log b o).2 +
      foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0
        (CNF b (o % b ^ log b o)) =
    o
refine_2₂ : b ^ (log b o, o / b ^ log b o).1 * (log b o, o / b ^ log b o).2 + o % b ^ log b o = o
⊢ foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o
have refine_2₃ : o = o
Tactic: rw [CNF.ne_zero ho, foldr_cons, IH, div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.1 ≤ log b o
have refine_1 : x ∈ CNF b 0 → x.1 ≤ log b 0
Tactic: refine CNF.rec b ?_ (fun o ho H ↦ ?_) o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
refine_1 : x ∈ CNF b 0 → x.1 ≤ log b 0
⊢ x ∈ CNF b o → x.1 ≤ log b o
have refine_2 : ∀ (o : Ordinal.{u}) (ho : o ≠ 0) (H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)),
  x ∈ CNF b o → x.1 ≤ log b o
Tactic: refine CNF.rec b ?_ (fun o ho H ↦ ?_) o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
⊢ x ∈ CNF b o → x.1 ≤ log b o
have refine_2 : x = (log b o, o / b ^ log b o) ∨ x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b o
Tactic: rw [CNF.ne_zero ho, mem_cons]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → 0 < x.2
have refine : ∀ (o : Ordinal.{u}) (ho : o ≠ 0) (IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2), x ∈ CNF b o → 0 < x.2
Tactic: refine CNF.rec b (by simp) (fun o ho IH ↦ ?_) o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2
⊢ x ∈ CNF b o → 0 < x.2
have rw : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.2
Tactic: rw [CNF.ne_zero ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.2 < b
have refine_1 : x ∈ CNF b 0 → x.2 < b
Tactic: refine CNF.rec b ?_ (fun o ho IH ↦ ?_) o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
refine_1 : x ∈ CNF b 0 → x.2 < b
⊢ x ∈ CNF b o → x.2 < b
have refine_2 : ∀ (o : Ordinal.{u}) (ho : o ≠ 0) (IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b), x ∈ CNF b o → x.2 < b
Tactic: refine CNF.rec b ?_ (fun o ho IH ↦ ?_) o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b
have refine_2 : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.2 < b
Tactic: rw [CNF.ne_zero ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
h : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ x.2 < b
have refine_2 : ∀ (IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).2 < b)
  (h : (log b o, o / b ^ log b o) ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)),
  (log b o, o / b ^ log b o).2 < b
Tactic: obtain rfl | h := mem_cons.mp h
Cleared hypotheses: x, IH, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).SortedGT
have simp_rw : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
Tactic: simp_rw [sortedGT_iff_pairwise]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
have refine_1 : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b 0))
Tactic: refine CNF.rec b ?_ (fun o ho IH ↦ ?_) o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
refine_1 : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b 0))
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
have refine_2 : ∀ (o : Ordinal.{u_1}) (ho : o ≠ 0)
  (IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))),
  List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
Tactic: refine CNF.rec b ?_ (fun o ho IH ↦ ?_) o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b 0))
have refine_1 : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map (α := Ordinal.{u_1} × Ordinal.{u_1}) Prod.fst [])
Tactic: rw [zero_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
have refine_2 : ∀ (hb : b ≤ 1), List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
refine_2 : ∀ (hb : b ≤ 1), List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
have refine_2₁ : ∀ (hb : 1 < b), List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
have refine_2 : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst [(0, o)])
Tactic: rw [CNF.of_le_one hb ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
have refine_2 : ∀ (hob : o < b), List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
Tactic: obtain hob | hbo := lt_or_ge o b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
refine_2 : ∀ (hob : o < b), List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
have refine_2₁ : ∀ (hbo : b ≤ o), List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
Tactic: obtain hob | hbo := lt_or_ge o b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
have refine_2 : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst [(0, o)])
Tactic: rw [CNF.of_lt ho hob]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
have refine_2 : (∀ a' ∈ map Prod.fst (CNF b (o % b ^ log b o)), (log b o, o / b ^ log b o).1 > a') ∧
  List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
Tactic: rw [CNF.ne_zero ho, map_cons, pairwise_cons]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ (∀ a' ∈ map Prod.fst (CNF b (o % b ^ log b o)), (log b o, o / b ^ log b o).1 > a') ∧
    List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
have refine_2 : ∀ (a : Ordinal.{u_1}) (H : a ∈ map Prod.fst (CNF b (o % b ^ log b o))), (log b o, o / b ^ log b o).1 > a
Tactic: refine ⟨fun a H ↦ ?_, IH⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (hypothesis)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal.{u_1}
H : a ∈ map Prod.fst (CNF b (o % b ^ log b o))
⊢ (log b o, o / b ^ log b o).1 > a
have H₁ : ∃ a_1 ∈ CNF b (o % b ^ log b o), a_1.1 = a
Tactic: rw [mem_map] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o_1 o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal.{u_1}
H : ∃ a_1 ∈ CNF b (o % b ^ log b o), a_1.1 = a
⊢ (log b o, o / b ^ log b o).1 > a
have refine_2 : ∀ (a a' : Ordinal.{u_1}) (H : (a, a') ∈ CNF b (o % b ^ log b o)), (log b o, o / b ^ log b o).1 > (a, a').1
Tactic: rcases H with ⟨⟨a, a'⟩, H, rfl⟩
Cleared hypotheses: a, H
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
⊢ (map Prod.toSigma (CNF b o)).NodupKeys (β := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1})
have rw : (map Prod.fst (CNF b o)).Nodup
Tactic: rw [NodupKeys, List.keys, map_map, Prod.fst_comp_toSigma]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
⊢ (coeff b o).support = (map Prod.fst (CNF b o)).toFinset
have rw : (AList.mk (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (map Prod.toSigma (CNF b o)) sorry).entries (β :=
          fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}).keys
      (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}).toFinset =
  (map Prod.fst (CNF b o)).toFinset
Tactic: rw [coeff, lookupFinsupp_support, filter_eq_self.2]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
rw :
  (AList.mk (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (map Prod.toSigma (CNF b o)) ⋯).entries (β :=
            fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}).keys
        (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}).toFinset =
    (map Prod.fst (CNF b o)).toFinset
⊢ (coeff b o).support = (map Prod.fst (CNF b o)).toFinset
have rw₁ : ∀
  a ∈
    (AList.mk (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (map Prod.toSigma (CNF b o)) sorry).entries (β :=
      fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}),
  decide (a.snd (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) ≠ 0) = true
Tactic: rw [coeff, lookupFinsupp_support, filter_eq_self.2]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o : Ordinal.{u_1}
⊢ ∀
    a ∈
      (AList.mk (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (map Prod.toSigma (CNF b o)) ⋯).entries (β :=
        fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}),
    decide (a.snd (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) ≠ 0) = true
have simp_rw : ∀ (a : (_ : Ordinal.{u_1}) × Ordinal.{u_1}),
  (∃ a_1 ∈ CNF b o, a_1.toSigma = a) → decide (a.snd (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) ≠ 0) = true
Tactic: simp_rw [mem_map]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ (coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = c
have rw : Sigma.mk (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) e c ∈
  (AList.mk (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (map Prod.toSigma (CNF b o)) sorry).entries (β :=
    fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1})
Tactic: rw [coeff, lookupFinsupp_apply, mem_lookup_iff.2, Option.getD_some]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
have rwa : e ∉ (coeff b o).support
Tactic: rwa [← notMem_support_iff, support_coeff, mem_toFinset]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
rwa : e ∉ (coeff b o).support
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
have rwa₁ : e ∉ (map Prod.fst (CNF b o)).toFinset
Tactic: rwa [← notMem_support_iff, support_coeff, mem_toFinset]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o e : Ordinal.{u_1}
h : o < b ^ e
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
have h₁ : e ∉ map Prod.fst (CNF b o)
Tactic: apply coeff_of_notMem_CNF
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (hypothesis)
Goal:
b o e : Ordinal.{u_1}
h : o < b ^ e
he : e ∈ map Prod.fst (CNF b o)
⊢ False
have he₁ : ∃ a ∈ CNF b o, a.1 = e
Tactic: rw [mem_map] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o e : Ordinal.{u_1}
h : o < b ^ e
he : ∃ a ∈ CNF b o, a.1 = e
⊢ False
have h₁ : ∀ (e c : Ordinal.{u_1}) (he : (e, c) ∈ CNF b o) (h : o < b ^ (e, c).1), False
Tactic: obtain ⟨⟨e, c⟩, he, rfl⟩ := he
Cleared hypotheses: e, h, he
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
⊢ False
have h₁ : ∀ (he : (0, c) ∈ CNF b o) (h : o < HPow.hPow (β := Ordinal.{u_1}) b (0, c).1), False
Tactic: obtain rfl | he' := eq_or_ne e 0
Cleared hypotheses: e, he, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
h₁ : ∀ (he : (0, c) ∈ CNF b o) (h : o < HPow.hPow (β := Ordinal.{u_1}) b (0, c).1), False
⊢ False
have h₂ : ∀ (he' : e ≠ 0), False
Tactic: obtain rfl | he' := eq_or_ne e 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b e : Ordinal.{u_1}
⊢ Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1}) (0 : Ordinal.{u_1})
have h : e ∉ map Prod.fst (CNF b 0)
Tactic: apply coeff_of_notMem_CNF
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
⊢ coeff b 0 = 0
have h : ∀ (e : Ordinal.{u_1}),
  Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
    ((0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e : Ordinal.{u_1})
Tactic: ext e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
⊢ coeff b o = single 0 o
have h : ∀ (a : Ordinal.{u_1}),
  Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
Tactic: ext a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
have h : Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
  ((single 0 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
Tactic: obtain rfl | ho := eq_or_ne o 0
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
h :
  Eq (α := Ordinal.{u_1}) ((coeff b 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
have h₁ : ∀ (ho : o ≠ 0),
  Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
Tactic: obtain rfl | ho := eq_or_ne o 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
have h : Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
  ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
h :
  Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
⊢ Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
have h₁ : ∀ (ha : a ≠ 0),
  Eq (α := Ordinal.{u_1}) ((coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
    ((single 0 o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
Tactic: obtain rfl | ha := eq_or_ne a 0