-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem CNF_sorted (b o : Ordinal) : ((CNF b o).map Prod.fst).Sorted (· > ·)

Proof state:
b o : Ordinal.{u_1}
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

Tactic:
refine CNFRec b ?_ (fun o ho IH ↦ ?_) o

Result:
case refine_1
b o : Ordinal.{u_1}
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b 0))

case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

Proof state:
case refine_2.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst [(0, o)])

Tactic:
exact sorted_singleton _

Result:
no goals

Proof state:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ (∀ b_1 ∈ map Prod.fst (CNF b (o % b ^ log b o)), (log b o, o / b ^ log b o).1 > b_1) ∧
    Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))

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

Result:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => 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

Proof state:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => 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

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

Result:
case refine_2.inr.inr.intro.mk.intro
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => 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

Proof state:
case refine_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst [(0, o)])

Tactic:
exact sorted_singleton _

Result:
no goals

Proof state:
case refine_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF_of_lt ho hob]

Result:
case refine_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst [(0, o)])

Proof state:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF_ne_zero ho, map_cons, sorted_cons]

Result:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ (∀ b_1 ∈ map Prod.fst (CNF b (o % b ^ log b o)), (log b o, o / b ^ log b o).1 > b_1) ∧
    Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))

Proof state:
case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case refine_2.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

case refine_2.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

Proof state:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => 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

Tactic:
rw [mem_map] at H

Result:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => 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

Proof state:
case refine_2.inr.inr.intro.mk.intro
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => 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 (CNF_fst_le_log H).trans_lt (log_mod_opow_log_lt_log_self hb hbo)

Result:
no goals

Proof state:
case refine_1
b o : Ordinal.{u_1}
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b 0))

Tactic:
rw [CNF_zero]

Result:
case refine_1
b o : Ordinal.{u_1}
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst [])

Proof state:
case refine_1
b o : Ordinal.{u_1}
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst [])

Tactic:
exact sorted_nil

Result:
no goals

Proof state:
case refine_2.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF_of_le_one hb ho]

Result:
case refine_2.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst [(0, o)])

Proof state:
case refine_2.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

Tactic:
obtain hob | hbo := lt_or_le o b

Result:
case refine_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))

case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ Sorted (fun x1 x2 => x1 > x2) (map Prod.fst (CNF b o))