[GOAL]
b : Ordinal.{?u.2}
C : Ordinal.{?u.2} → Sort u_1
H0 : C 0
H : (o : Ordinal.{?u.2}) → o ≠ 0 → C (o % b ^ log b o) → C o
o : Ordinal.{?u.2}
⊢ C o
[PROOFSTEP]
by_cases h : o = 0
[GOAL]
case pos
b : Ordinal.{?u.2}
C : Ordinal.{?u.2} → Sort u_1
H0 : C 0
H : (o : Ordinal.{?u.2}) → o ≠ 0 → C (o % b ^ log b o) → C o
o : Ordinal.{?u.2}
h : o = 0
⊢ C o
[PROOFSTEP]
rw [h]
[GOAL]
case pos
b : Ordinal.{?u.2}
C : Ordinal.{?u.2} → Sort u_1
H0 : C 0
H : (o : Ordinal.{?u.2}) → o ≠ 0 → C (o % b ^ log b o) → C o
o : Ordinal.{?u.2}
h : o = 0
⊢ C 0
[PROOFSTEP]
exact H0
[GOAL]
case neg
b : Ordinal.{?u.2}
C : Ordinal.{?u.2} → Sort u_1
H0 : C 0
H : (o : Ordinal.{?u.2}) → o ≠ 0 → C (o % b ^ log b o) → C o
o : Ordinal.{?u.2}
h : ¬o = 0
⊢ C o
[PROOFSTEP]
exact H o h (CNFRec _ H0 H (o % b ^ log b o))
[GOAL]
b o : Ordinal.{u_2}
h : ¬o = 0
⊢ (invImage (fun a => a) wellFoundedRelation).1 (o % b ^ log b o) o
[PROOFSTEP]
exact mod_opow_log_lt_self b h
[GOAL]
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNFRec b H0 H 0 = H0
[PROOFSTEP]
rw [CNFRec, dif_pos rfl]
[GOAL]
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ Eq.mpr (_ : C 0 = C 0) H0 = H0
[PROOFSTEP]
rfl
[GOAL]
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNFRec b H0 H o = H o ho (CNFRec b H0 H (o % b ^ log b o))
[PROOFSTEP]
rw [CNFRec, dif_neg ho]
[GOAL]
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 0 o = [(0, o)]
[PROOFSTEP]
simp [CNF_ne_zero ho]
[GOAL]
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 1 o = [(0, o)]
[PROOFSTEP]
simp [CNF_ne_zero ho]
[GOAL]
b o : Ordinal.{u_1}
hb : b ≤ 1
ho : o ≠ 0
⊢ CNF b o = [(0, o)]
[PROOFSTEP]
rcases le_one_iff.1 hb with (rfl | rfl)
[GOAL]
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 ≤ 1
⊢ CNF 0 o = [(0, o)]
[PROOFSTEP]
exact zero_CNF ho
[GOAL]
case inr
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 1 ≤ 1
⊢ CNF 1 o = [(0, o)]
[PROOFSTEP]
exact one_CNF ho
[GOAL]
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ CNF b o = [(0, o)]
[PROOFSTEP]
simp only [CNF_ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, CNF_zero]
[GOAL]
b o : Ordinal.{u_1}
⊢ foldr (fun p r => b ^ p.fst * p.snd + r) 0 (CNF b 0) = 0
[PROOFSTEP]
rw [CNF_zero]
[GOAL]
b o : Ordinal.{u_1}
⊢ foldr (fun p r => b ^ p.fst * p.snd + r) 0 [] = 0
[PROOFSTEP]
rfl
[GOAL]
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : foldr (fun p r => b ^ p.fst * p.snd + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o
⊢ foldr (fun p r => b ^ p.fst * p.snd + r) 0 (CNF b o) = o
[PROOFSTEP]
rw [CNF_ne_zero ho, foldr_cons, IH, div_add_mod]
[GOAL]
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.fst ≤ log b o
[PROOFSTEP]
refine' CNFRec b _ (fun o ho H ↦ _) o
[GOAL]
case refine'_1
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.fst ≤ log b 0
[PROOFSTEP]
rw [CNF_zero]
[GOAL]
case refine'_1
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ [] → x.fst ≤ log b 0
[PROOFSTEP]
intro contra
[GOAL]
case refine'_1
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
contra : x ∈ []
⊢ x.fst ≤ log b 0
[PROOFSTEP]
contradiction
[GOAL]
case refine'_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
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
[PROOFSTEP]
rw [CNF_ne_zero ho, mem_cons]
[GOAL]
case refine'_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
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
[PROOFSTEP]
rintro (rfl | h)
[GOAL]
case refine'_2.inl
b o✝ 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).fst ≤ log b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).fst ≤ log b o
[PROOFSTEP]
exact le_rfl
[GOAL]
case refine'_2.inr
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
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
[PROOFSTEP]
exact (H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)
[GOAL]
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → 0 < x.snd
[PROOFSTEP]
refine' CNFRec b (by simp) (fun o ho IH ↦ _) o
[GOAL]
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → 0 < x.snd
[PROOFSTEP]
simp
[GOAL]
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
⊢ x ∈ CNF b o → 0 < x.snd
[PROOFSTEP]
rw [CNF_ne_zero ho]
[GOAL]
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.snd
[PROOFSTEP]
rintro (h | ⟨_, h⟩)
[GOAL]
case head
b o✝ 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).snd
⊢ 0 < (log b o, o / b ^ log b o).snd
[PROOFSTEP]
exact div_opow_log_pos b ho
[GOAL]
case tail
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
h : Mem x (CNF b (o % b ^ log b o))
⊢ 0 < x.snd
[PROOFSTEP]
exact IH h
[GOAL]
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.snd < b
[PROOFSTEP]
refine' CNFRec b _ (fun o ho IH ↦ _) o
[GOAL]
case refine'_1
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.snd < b
[PROOFSTEP]
simp only [CNF_zero, not_mem_nil, IsEmpty.forall_iff]
[GOAL]
case refine'_2
b o✝ : 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.snd < b
⊢ x ∈ CNF b o → x.snd < b
[PROOFSTEP]
rw [CNF_ne_zero ho]
[GOAL]
case refine'_2
b o✝ : 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.snd < b
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.snd < b
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
b o✝ : 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.snd < b
h : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ x.snd < b
[PROOFSTEP]
cases' (mem_cons.mp h) with h h
[GOAL]
case refine'_2.inl
b o✝ : 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.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
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_2.inl
b o✝ : 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.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
[PROOFSTEP]
simpa only using div_opow_log_lt o hb
[GOAL]
case refine'_2.inr
b o✝ : 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.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
[PROOFSTEP]
exact IH h
[GOAL]
b o : Ordinal.{u_1}
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b o))
[PROOFSTEP]
refine' CNFRec b _ (fun o ho IH ↦ _) o
[GOAL]
case refine'_1
b o : Ordinal.{u_1}
⊢ Sorted (fun x x_1 => x > x_1) (map Prod.fst (CNF b 0))
[PROOFSTEP]
simp only [CNF_zero]
[GOAL]
case refine'_2
b o✝ o : Ordinal.{u_1}
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))
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case refine'_2.inl
b o✝ o : Ordinal.{u_1}
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))
[PROOFSTEP]
simp only [CNF_of_le_one hb ho, map]
[GOAL]
case refine'_2.inr
b o✝ o : Ordinal.{u_1}
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))
[PROOFSTEP]
cases' lt_or_le o b with hob hbo
[GOAL]
case refine'_2.inr.inl
b o✝ o : Ordinal.{u_1}
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))
[PROOFSTEP]
simp only [CNF_of_lt ho hob, map]
[GOAL]
case refine'_2.inr.inr
b o✝ o : Ordinal.{u_1}
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))
[PROOFSTEP]
rw [CNF_ne_zero ho, map_cons, sorted_cons]
[GOAL]
case refine'_2.inr.inr
b o✝ o : Ordinal.{u_1}
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.{u_1}), 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)))
[PROOFSTEP]
refine' ⟨fun a H ↦ _, IH⟩
[GOAL]
case refine'_2.inr.inr
b o✝ o : Ordinal.{u_1}
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.{u_1}
H : a ∈ map Prod.fst (CNF b (o % b ^ log b o))
⊢ (log b o, o / b ^ log b o).fst > a
[PROOFSTEP]
rw [mem_map] at H 
[GOAL]
case refine'_2.inr.inr
b o✝ o : Ordinal.{u_1}
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.{u_1}
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
[PROOFSTEP]
rcases H with ⟨⟨a, a'⟩, H, rfl⟩
[GOAL]
case refine'_2.inr.inr.intro.mk.intro
b o✝ o : Ordinal.{u_1}
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.{u_1}
H : (a, a') ∈ CNF b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).fst > (a, a').fst
[PROOFSTEP]
exact (CNF_fst_le_log H).trans_lt (log_mod_opow_log_lt_log_self hb ho hbo)
