awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)]
rw₅ rw₆ : Eq (α := List (Ordinal.{u_1} × Ordinal.{u_1})) [(0, o)] [(0, o)]
⊢ CNF b o = [(0, o)]

Tactic:
rw [CNF.ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, zero_right]

Premises used: Ordinal.log_eq_zero, Ordinal.mod_one, Ordinal.opow_zero, Ordinal.CNF.ne_zero, Ordinal.CNF.zero_right, Ordinal.div_one
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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

Tactic:
CNF.rec b ?_ ?_ o

Premises used: Ordinal.CNF.rec
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
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
⊢ 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
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
refine_1₁ refine_1₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 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

Tactic:
rw [zero_right, foldr_nil]

Premises used: List.foldr_nil, Ordinal.CNF.zero_right
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
refine_2₃ refine_2₄ : 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

Tactic:
rw [CNF.ne_zero ho, foldr_cons, IH, div_add_mod]

Premises used: List.foldr_cons, Ordinal.div_add_mod, Ordinal.CNF.ne_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.1 ≤ log b o

Tactic:
CNF.rec b ?_ (fun o ho H ↦ ?_) o

Premises used: Ordinal.CNF.rec
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
refine_1 : x ∈ CNF b 0 → x.1 ≤ log b 0
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
⊢ x ∈ CNF b o → x.1 ≤ log b o

Tactic:
refine CNF.rec b ?_ (fun o ho H ↦ ?_) o
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.1 ≤ log b 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)
refine_2 : x = (log b o, o / b ^ log b o) ∨ x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b o
⊢ x ∈ CNF b o → x.1 ≤ log b o

Tactic:
rw [CNF.ne_zero ho, mem_cons]

Premises used: Ordinal.CNF.ne_zero, List.mem_cons
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o_1 o : Ordinal.{u}
ho : o ≠ 0
H : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).1 ≤ log b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).1 ≤ (log b o, o / b ^ log b o).1

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.1 ≤ log b o

Tactic:
(H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)

Premises used: LT.lt.le, Ordinal.log_mono_right, Ordinal.mod_opow_log_lt_self, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.1 ≤ log b o

Tactic:
exact (H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)

Premises used: LT.lt.le, Ordinal.log_mono_right, Ordinal.mod_opow_log_lt_self, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → 0 < x.2

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
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
⊢ x ∈ CNF b o → 0 < x.2

Tactic:
refine CNF.rec b (by simp) (fun o ho IH ↦ ?_) o
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
rw : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.2
⊢ x ∈ CNF b o → 0 < x.2

Tactic:
rw [CNF.ne_zero ho]

Premises used: Ordinal.CNF.ne_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o_1 o : Ordinal.{u}
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → 0 < (log b o, o / b ^ log b o).2
⊢ 0 < (log b o, o / b ^ log b o).2

Tactic:
div_opow_log_pos b ho

Premises used: Ordinal.div_opow_log_pos
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o_1 o : Ordinal.{u}
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → 0 < (log b o, o / b ^ log b o).2
⊢ 0 < (log b o, o / b ^ log b o).2

Tactic:
exact div_opow_log_pos b ho

Premises used: Ordinal.div_opow_log_pos
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
h : Mem x (CNF b (o % b ^ log b o))
⊢ 0 < x.2

Tactic:
IH h
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
h : Mem x (CNF b (o % b ^ log b o))
⊢ 0 < x.2

Tactic:
exact IH h
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.2 < b

Tactic:
CNF.rec b ?_ (fun o ho IH ↦ ?_) o

Premises used: Ordinal.CNF.rec
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
refine_1 : x ∈ CNF b 0 → x.2 < b
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
⊢ x ∈ CNF b o → x.2 < b

Tactic:
refine CNF.rec b ?_ (fun o ho IH ↦ ?_) o
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.2 < b

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
refine_2 : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b

Tactic:
rw [CNF.ne_zero ho]

Premises used: Ordinal.CNF.ne_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)
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
refine_2₁ : ∀ (h : x ∈ CNF b (o % b ^ log b o)), x.2 < b
⊢ x.2 < b

Tactic:
obtain rfl | h := mem_cons.mp h

Premises used: Iff.mp, List.mem_cons, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o_1 : Ordinal.{u}
hb : 1 < b
o : Ordinal.{u}
ho : o ≠ 0
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:
div_opow_log_lt o hb

Premises used: Ordinal.div_opow_log_lt
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o_1 : Ordinal.{u}
hb : 1 < b
o : Ordinal.{u}
ho : o ≠ 0
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:
exact div_opow_log_lt o hb

Premises used: Ordinal.div_opow_log_lt
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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_1 : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.2 < b

Tactic:
IH h
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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_1 : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.2 < b

Tactic:
exact IH h
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
simp_rw : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))
⊢ (map Prod.fst (CNF b o)).SortedGT

Tactic:
simp_rw [sortedGT_iff_pairwise]

Premises used: List.sortedGT_iff_pairwise
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
CNF.rec b ?_ (fun o ho IH ↦ ?_) o

Premises used: Ordinal.CNF.rec
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
refine_1 : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b 0))
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))
⊢ 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
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
refine_1 : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map (α := Ordinal.{u_1} × Ordinal.{u_1}) Prod.fst [])
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b 0))

Tactic:
rw [zero_right]

Premises used: Ordinal.CNF.zero_right
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map (α := Ordinal.{u_1} × Ordinal.{u_1}) Prod.fst [])

Tactic:
.nil

Premises used: List.map, List.Pairwise.nil
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map (α := Ordinal.{u_1} × Ordinal.{u_1}) Prod.fst [])

Tactic:
exact .nil
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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))
refine_2₁ : ∀ (hb : 1 < 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))

Tactic:
rcases le_or_gt b 1 with hb | hb

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
refine_2 : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst [(0, o)])
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF.of_le_one hb ho]

Premises used: Ordinal.CNF.of_le_one
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 [(0, o)])

Tactic:
pairwise_singleton _ _

Premises used: List.map, List.pairwise_singleton
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 [(0, o)])

Tactic:
exact pairwise_singleton _ _

Premises used: List.pairwise_singleton
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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))
refine_2₁ : ∀ (hbo : b ≤ o), 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))

Tactic:
obtain hob | hbo := lt_or_ge o b

Premises used: lt_or_ge
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
refine_2 : List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst [(0, o)])
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF.of_lt ho hob]

Premises used: Ordinal.CNF.of_lt
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 [(0, o)])

Tactic:
pairwise_singleton _ _

Premises used: List.map, List.pairwise_singleton
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 [(0, o)])

Tactic:
exact pairwise_singleton _ _

Premises used: List.pairwise_singleton
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
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)))
⊢ List.Pairwise (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF.ne_zero ho, map_cons, pairwise_cons]

Premises used: List.map_cons, List.pairwise_cons, Ordinal.CNF.ne_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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)))

Tactic:
⟨fun a H ↦ ?_, IH⟩

Premises used: And.intro
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
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
⊢ (∀ 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:
refine ⟨fun a H ↦ ?_, IH⟩
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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))
⊢ ∃ a_1 ∈ CNF b (o % b ^ log b o), a_1.1 = a

Tactic:
rw [mem_map] at H

Premises used: List.mem_map
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
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
⊢ (log b o, o / b ^ log b o).1 > a

Tactic:
rcases H with ⟨⟨a, a'⟩, H, rfl⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 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:
(fst_le_log H).trans_lt (log_mod_opow_log_lt_log_self hb hbo)

Premises used: Ordinal.log_mod_opow_log_lt_log_self, Ordinal.CNF.fst_le_log, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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 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:
exact (fst_le_log H).trans_lt (log_mod_opow_log_lt_log_self hb hbo)

Premises used: Ordinal.log_mod_opow_log_lt_log_self, Ordinal.CNF.fst_le_log, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
rw : (map Prod.fst (CNF b o)).Nodup
⊢ (map Prod.toSigma (CNF b o)).NodupKeys (β := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1})

Tactic:
rw [NodupKeys, List.keys, map_map, Prod.fst_comp_toSigma]

Premises used: Prod.fst_comp_toSigma, List.keys, List.map_map, List.NodupKeys
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).Nodup

Tactic:
(CNF.sortedGT ..).nodup

Premises used: List.SortedGT.nodup, Ordinal.CNF.sortedGT
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).Nodup

Tactic:
exact (CNF.sortedGT ..).nodup

Premises used: List.SortedGT.nodup, Ordinal.CNF.sortedGT
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
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
rw₁ :
  ∀
    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
⊢ (coeff b o).support = (map Prod.fst (CNF b o)).toFinset

Tactic:
rw [coeff, lookupFinsupp_support, filter_eq_self.2]

Premises used: Iff.mpr, Ordinal.CNF.coeff, List.filter_eq_self, AList.lookupFinsupp_support
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
⊢ (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

Tactic:
simp [List.keys]

Premises used: List.keys
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
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
⊢ ∀
    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

Tactic:
simp_rw [mem_map]

Premises used: List.mem_map
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
⊢ decide (a.toSigma.snd (β := fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) ≠ 0) = true

Tactic:
simpa using (snd_pos ha).ne'

Premises used: LT.lt.ne', Ordinal.CNF.snd_pos
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
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)) ⋯).entries (β :=
      fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1})
⊢ (coeff b o : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = c

Tactic:
rw [coeff, lookupFinsupp_apply, mem_lookup_iff.2, Option.getD_some]

Premises used: Iff.mpr, Ordinal.CNF.coeff, Option.getD_some, AList.lookupFinsupp_apply, AList.mem_lookup_iff
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ 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)) ⋯).entries (β :=
      fun (_x : Ordinal.{u_1}) ↦ Ordinal.{u_1})

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
rwa : e ∉ (coeff b o).support
rwa₁ : e ∉ (map Prod.fst (CNF b o)).toFinset
rwa₂ rwa₃ rwa₄ rwa₅ : 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})

Tactic:
rwa [← notMem_support_iff, support_coeff, mem_toFinset]

Premises used: List.mem_toFinset, Finsupp.notMem_support_iff, Ordinal.CNF.support_coeff
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o e : Ordinal.{u_1}
h : o < b ^ e
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})

Tactic:
apply coeff_of_notMem_CNF

Premises used: Ordinal.CNF.coeff_of_notMem_CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o e : Ordinal.{u_1}
h : o < b ^ e
he : e ∈ map Prod.fst (CNF b o)
⊢ ∃ a ∈ CNF b o, a.1 = e

Tactic:
rw [mem_map] at he

Premises used: List.mem_map
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o e : Ordinal.{u_1}
h : o < b ^ e
he : ∃ a ∈ CNF b o, a.1 = e
h₁ : ∀ (e c : Ordinal.{u_1}) (he : (e, c) ∈ CNF b o) (h : o < b ^ (e, c).1), False
⊢ False

Tactic:
obtain ⟨⟨e, c⟩, he, rfl⟩ := he

Premises used: rfl