case refine'_1
b o : Ordinal
x : Ordinal × Ordinal
⊢ x ∈ CNF b 0 → x.fst ≤ log b 0

case refine'_2
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b (o % b ^ log b o)
⊢ x ∈ CNF b o → x.fst ≤ log b o
b o : Ordinal
x : Ordinal × Ordinal
⊢ x ∈ CNF b o → x.fst ≤ log b o
refine' CNFRec b _ (fun o ho H ↦ _) o
case refine'_1
b o : Ordinal
x : Ordinal × Ordinal
⊢ x ∈ [] → x.fst ≤ log b 0
case refine'_1
b o : Ordinal
x : Ordinal × Ordinal
⊢ x ∈ CNF b 0 → x.fst ≤ log b 0
rw [CNF_zero]
case refine'_1
b o : Ordinal
x : Ordinal × Ordinal
contra : x ∈ []
⊢ x.fst ≤ log b 0
case refine'_1
b o : Ordinal
x : Ordinal × Ordinal
⊢ x ∈ [] → x.fst ≤ log b 0
intro contra
no goals
case refine'_1
b o : Ordinal
x : Ordinal × Ordinal
contra : x ∈ []
⊢ x.fst ≤ log b 0
contradiction
case refine'_2
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b (o % b ^ log b o)
⊢ x = (log b o, o / b ^ log b o) ∨ x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b o
case refine'_2
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b (o % b ^ log b o)
⊢ x ∈ CNF b o → x.fst ≤ log b o
rw [CNF_ne_zero ho, mem_cons]
case refine'_2.inl
b o✝ o : Ordinal
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).fst ≤ log b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).fst ≤ log b o

case refine'_2.inr
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.fst ≤ log b o
case refine'_2
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b (o % b ^ log b o)
⊢ x = (log b o, o / b ^ log b o) ∨ x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b o
rintro (rfl | h)
no goals
case refine'_2.inl
b o✝ o : Ordinal
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).fst ≤ log b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).fst ≤ log b o
exact le_rfl
no goals
case refine'_2.inr
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.fst ≤ log b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.fst ≤ log b o
exact (H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)