case refine'_1
b o : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
⊢ x ∈ CNF b 0 → x.snd < b

case refine'_2
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
⊢ x ∈ CNF b o → x.snd < b
b o : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
⊢ x ∈ CNF b o → x.snd < b
refine' CNFRec b _ (fun o ho IH ↦ _) o
no goals
case refine'_1
b o : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
⊢ x ∈ CNF b 0 → x.snd < b
simp only [CNF_zero, not_mem_nil, IsEmpty.forall_iff]
case refine'_2
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.snd < b
case refine'_2
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
⊢ x ∈ CNF b o → x.snd < b
rw [CNF_ne_zero ho]
case refine'_2
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ x.snd < b
case refine'_2
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.snd < b
intro h
case refine'_2.inl
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x = (log b o, o / b ^ log b o)
⊢ x.snd < b

case refine'_2.inr
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h✝ : 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.snd < b
case refine'_2
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ x.snd < b
cases' (mem_cons.mp h) with h h
case refine'_2.inl
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x = (log b o, o / b ^ log b o)
⊢ (log b o, o / b ^ log b o).snd < b
case refine'_2.inl
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x = (log b o, o / b ^ log b o)
⊢ x.snd < b
rw [h]
no goals
case refine'_2.inl
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x = (log b o, o / b ^ log b o)
⊢ (log b o, o / b ^ log b o).snd < b
simpa only using div_opow_log_lt o hb
no goals
case refine'_2.inr
b o✝ : Ordinal
hb : 1 < b
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.snd < b
h✝ : 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.snd < b
exact IH h