case refine'_1
b o : Ordinal
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b 0))

case refine'_2
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
b o : Ordinal
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
refine' CNFRec b _ (fun o ho IH ↦ _) o
no goals
case refine'_1
b o : Ordinal
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b 0))
simp only [CNF_zero]
case refine'_2.inl
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))

case refine'_2.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
case refine'_2
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
cases' le_or_lt b 1 with hb hb
no goals
case refine'_2.inl
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
simp only [CNF_of_le_one hb ho, map]
case refine'_2.inr.inl
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))

case refine'_2.inr.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
case refine'_2.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
cases' lt_or_le o b with hob hbo
no goals
case refine'_2.inr.inl
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
simp only [CNF_of_lt ho hob, map]
case refine'_2.inr.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ (∀ (b_1 : Ordinal), b_1 ∈ map Prod.fst (CNF b (o % b ^ log b o)) → (log b o, o / b ^ log b o).fst > b_1) ∧
    Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
case refine'_2.inr.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
rw [CNF_ne_zero ho, map_cons, sorted_cons]
case refine'_2.inr.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal
H : a ∈ map Prod.fst (CNF b (o % b ^ log b o))
⊢ (log b o, o / b ^ log b o).fst > a
case refine'_2.inr.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ (∀ (b_1 : Ordinal), b_1 ∈ map Prod.fst (CNF b (o % b ^ log b o)) → (log b o, o / b ^ log b o).fst > b_1) ∧
    Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
refine' ⟨fun a H ↦ _, IH⟩
case refine'_2.inr.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal
H : ∃ a_1, a_1 ∈ CNF b (o % b ^ log b o) ∧ a_1.fst = a
⊢ (log b o, o / b ^ log b o).fst > a
case refine'_2.inr.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal
H : a ∈ map Prod.fst (CNF b (o % b ^ log b o))
⊢ (log b o, o / b ^ log b o).fst > a
rw [mem_map] at H
case refine'_2.inr.inr.intro.mk.intro
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a a' : Ordinal
H : (a, a') ∈ CNF b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).fst > (a, a').fst
case refine'_2.inr.inr
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a : Ordinal
H : ∃ a_1, a_1 ∈ CNF b (o % b ^ log b o) ∧ a_1.fst = a
⊢ (log b o, o / b ^ log b o).fst > a
rcases H with ⟨⟨a, a'⟩, H, rfl⟩
no goals
case refine'_2.inr.inr.intro.mk.intro
b o✝ o : Ordinal
ho : o ≠ 0
IH : Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
a a' : Ordinal
H : (a, a') ∈ CNF b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).fst > (a, a').fst
exact (CNF_fst_le_log H).trans_lt (log_mod_opow_log_lt_log_self hb ho hbo)