[GOAL]
b : ℕ
h : 2 ≤ b
n : ℕ
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 ((n + 1) / b) (succ n)
[PROOFSTEP]
exact Nat.div_lt_self (Nat.succ_pos _) h
[GOAL]
n b : ℕ
h : 2 ≤ b
⊢ digitsAux b h 0 = []
[PROOFSTEP]
rw [digitsAux]
[GOAL]
n✝ b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n
⊢ digitsAux b h n = n % b :: digitsAux b h (n / b)
[PROOFSTEP]
cases n
[GOAL]
case zero
n b : ℕ
h : 2 ≤ b
w : 0 < zero
⊢ digitsAux b h zero = zero % b :: digitsAux b h (zero / b)
[PROOFSTEP]
cases w
[GOAL]
case succ
n b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < succ n✝
⊢ digitsAux b h (succ n✝) = succ n✝ % b :: digitsAux b h (succ n✝ / b)
[PROOFSTEP]
rw [digitsAux]
[GOAL]
n b : ℕ
⊢ 2 ≤ b + 2
[PROOFSTEP]
norm_num
[GOAL]
n b : ℕ
⊢ digits b 0 = []
[PROOFSTEP]
rcases b with (_ | ⟨_ | ⟨_⟩⟩)
[GOAL]
case zero
n : ℕ
⊢ digits zero 0 = []
[PROOFSTEP]
simp [digits, digitsAux0, digitsAux1]
[GOAL]
case succ.zero
n : ℕ
⊢ digits (succ zero) 0 = []
[PROOFSTEP]
simp [digits, digitsAux0, digitsAux1]
[GOAL]
case succ.succ
n n✝ : ℕ
⊢ digits (succ (succ n✝)) 0 = []
[PROOFSTEP]
simp [digits, digitsAux0, digitsAux1]
[GOAL]
n✝ b n : ℕ
⊢ digits (b + 2) (n + 1) = (n + 1) % (b + 2) :: digits (b + 2) ((n + 1) / (b + 2))
[PROOFSTEP]
simp [digits, digitsAux_def]
[GOAL]
n n✝ : ℕ
h : 1 < 0
⊢ ¬1 < 0
[PROOFSTEP]
decide
[GOAL]
n n✝ : ℕ
h : 1 < 1
⊢ ¬1 < 1
[PROOFSTEP]
decide
[GOAL]
n n✝ b : ℕ
x✝ : 1 < b + 2
⊢ 2 ≤ Nat.add b 0 + 2
[PROOFSTEP]
simp
[GOAL]
n b x : ℕ
hx : x ≠ 0
hxb : x < b
⊢ digits b x = [x]
[PROOFSTEP]
rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩
[GOAL]
case intro
n b x : ℕ
hx : succ x ≠ 0
hxb : succ x < b
⊢ digits b (succ x) = [succ x]
[PROOFSTEP]
rcases exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩
[GOAL]
case intro.intro
n x : ℕ
hx : succ x ≠ 0
b : ℕ
hxb : succ x < b + succ 1
⊢ digits (b + succ 1) (succ x) = [succ x]
[PROOFSTEP]
rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]
[GOAL]
n b : ℕ
h : 1 < b
x y : ℕ
hxb : x < b
hxy : x ≠ 0 ∨ y ≠ 0
⊢ digits b (x + b * y) = x :: digits b y
[PROOFSTEP]
rcases exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩
[GOAL]
case intro
n x y : ℕ
hxy : x ≠ 0 ∨ y ≠ 0
b : ℕ
h : 1 < b + 2
hxb : x < b + 2
⊢ digits (b + 2) (x + (b + 2) * y) = x :: digits (b + 2) y
[PROOFSTEP]
cases y
[GOAL]
case intro.zero
n x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
hxy : x ≠ 0 ∨ zero ≠ 0
⊢ digits (b + 2) (x + (b + 2) * zero) = x :: digits (b + 2) zero
[PROOFSTEP]
simp [hxb, hxy.resolve_right (absurd rfl)]
[GOAL]
case intro.succ
n x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ succ n✝ ≠ 0
⊢ digits (b + 2) (x + (b + 2) * succ n✝) = x :: digits (b + 2) (succ n✝)
[PROOFSTEP]
dsimp [digits]
[GOAL]
case intro.succ
n x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ succ n✝ ≠ 0
⊢ digitsAux (b + 2) (_ : 2 ≤ b + 2) (x + (b + 2) * succ n✝) = x :: digitsAux (b + 2) (_ : 2 ≤ b + 2) (succ n✝)
[PROOFSTEP]
rw [digitsAux_def]
[GOAL]
case intro.succ
n x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ succ n✝ ≠ 0
⊢ (x + (b + 2) * succ n✝) % (b + 2) :: digitsAux (b + 2) (_ : 2 ≤ b + 2) ((x + (b + 2) * succ n✝) / (b + 2)) =
    x :: digitsAux (b + 2) (_ : 2 ≤ b + 2) (succ n✝)
[PROOFSTEP]
congr
[GOAL]
case intro.succ.e_head
n x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ succ n✝ ≠ 0
⊢ (x + (b + 2) * succ n✝) % (b + 2) = x
[PROOFSTEP]
simp [Nat.add_mod, mod_eq_of_lt hxb]
[GOAL]
case intro.succ.e_tail.e_a
n x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ succ n✝ ≠ 0
⊢ (x + (b + 2) * succ n✝) / (b + 2) = succ n✝
[PROOFSTEP]
simp [add_mul_div_left, div_eq_of_lt hxb]
[GOAL]
case intro.succ.w
n x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ succ n✝ ≠ 0
⊢ 0 < x + (b + 2) * succ n✝
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
L : List ℕ
⊢ ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
[PROOFSTEP]
induction' L with d L ih
[GOAL]
case nil
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
⊢ ofDigits b [] = List.foldr (fun x y => ↑x + b * y) 0 []
[PROOFSTEP]
rfl
[GOAL]
case cons
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ofDigits b (d :: L) = List.foldr (fun x y => ↑x + b * y) 0 (d :: L)
[PROOFSTEP]
dsimp [ofDigits]
[GOAL]
case cons
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ↑d + b * ofDigits b L = ↑d + b * List.foldr (fun x y => ↑x + b * y) 0 L
[PROOFSTEP]
rw [ih]
[GOAL]
n b : ℕ
l : List ℕ
⊢ List.sum (List.zipWith ((fun i a => a * b ^ i) ∘ succ) (List.range (List.length l)) l) =
    b * List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length l)) l)
[PROOFSTEP]
suffices
  (List.range l.length).zipWith ((fun i a : ℕ => a * b ^ i) ∘ succ) l =
    (List.range l.length).zipWith (fun i a => b * (a * b ^ i)) l
  by simp [this]
[GOAL]
n b : ℕ
l : List ℕ
this :
  List.zipWith ((fun i a => a * b ^ i) ∘ succ) (List.range (List.length l)) l =
    List.zipWith (fun i a => b * (a * b ^ i)) (List.range (List.length l)) l
⊢ List.sum (List.zipWith ((fun i a => a * b ^ i) ∘ succ) (List.range (List.length l)) l) =
    b * List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length l)) l)
[PROOFSTEP]
simp [this]
[GOAL]
n b : ℕ
l : List ℕ
⊢ List.zipWith ((fun i a => a * b ^ i) ∘ succ) (List.range (List.length l)) l =
    List.zipWith (fun i a => b * (a * b ^ i)) (List.range (List.length l)) l
[PROOFSTEP]
congr
[GOAL]
case e_f
n b : ℕ
l : List ℕ
⊢ (fun i a => a * b ^ i) ∘ succ = fun i a => b * (a * b ^ i)
[PROOFSTEP]
ext
[GOAL]
case e_f.h.h
n b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ ((fun i a => a * b ^ i) ∘ succ) x✝¹ x✝ = b * (x✝ * b ^ x✝¹)
[PROOFSTEP]
simp [pow_succ]
[GOAL]
case e_f.h.h
n b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝ * (b ^ x✝¹ * b) = b * (x✝ * b ^ x✝¹)
[PROOFSTEP]
ring
[GOAL]
n b : ℕ
L : List ℕ
⊢ ofDigits b L = List.sum (List.mapIdx (fun i a => a * b ^ i) L)
[PROOFSTEP]
rw [List.mapIdx_eq_enum_map, List.enum_eq_zip_range, List.map_uncurry_zip_eq_zipWith, ofDigits_eq_foldr]
[GOAL]
n b : ℕ
L : List ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 L = List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length L)) L)
[PROOFSTEP]
induction' L with hd tl hl
[GOAL]
case nil
n b : ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 [] =
    List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length [])) [])
[PROOFSTEP]
simp
[GOAL]
case cons
n b hd : ℕ
tl : List ℕ
hl :
  List.foldr (fun x y => ↑x + b * y) 0 tl =
    List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length tl)) tl)
⊢ List.foldr (fun x y => ↑x + b * y) 0 (hd :: tl) =
    List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length (hd :: tl))) (hd :: tl))
[PROOFSTEP]
simpa [List.range_succ_eq_map, List.zipWith_map_left, ofDigits_eq_sum_map_with_index_aux] using Or.inl hl
[GOAL]
n✝ b n : ℕ
⊢ ofDigits b [n] = n
[PROOFSTEP]
simp [ofDigits]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : Semiring α
h : ℕ
L : List ℕ
⊢ ofDigits 1 (h :: L) = ↑h + ofDigits 1 L
[PROOFSTEP]
simp [ofDigits]
[GOAL]
n b : ℕ
l1 l2 : List ℕ
⊢ ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ List.length l1 * ofDigits b l2
[PROOFSTEP]
induction' l1 with hd tl IH
[GOAL]
case nil
n b : ℕ
l2 : List ℕ
⊢ ofDigits b ([] ++ l2) = ofDigits b [] + b ^ List.length [] * ofDigits b l2
[PROOFSTEP]
simp [ofDigits]
[GOAL]
case cons
n b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ List.length tl * ofDigits b l2
⊢ ofDigits b (hd :: tl ++ l2) = ofDigits b (hd :: tl) + b ^ List.length (hd :: tl) * ofDigits b l2
[PROOFSTEP]
rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']
[GOAL]
case cons
n b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ List.length tl * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ List.length tl * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b * b ^ List.length tl * ofDigits b l2
[PROOFSTEP]
ring
[GOAL]
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : ℕ
L : List ℕ
⊢ ↑(ofDigits b L) = ofDigits (↑b) L
[PROOFSTEP]
induction' L with d L ih
[GOAL]
case nil
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : ℕ
⊢ ↑(ofDigits b []) = ofDigits ↑b []
[PROOFSTEP]
simp [ofDigits]
[GOAL]
case cons
n : ℕ
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(ofDigits b (d :: L)) = ofDigits (↑b) (d :: L)
[PROOFSTEP]
dsimp [ofDigits]
[GOAL]
case cons
n : ℕ
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(d + b * ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L
[PROOFSTEP]
push_cast
[GOAL]
case cons
n : ℕ
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ↑(ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L
[PROOFSTEP]
rw [ih]
[GOAL]
n b : ℕ
L : List ℕ
⊢ ↑(ofDigits b L) = ofDigits (↑b) L
[PROOFSTEP]
induction' L with d L _
[GOAL]
case nil
n b : ℕ
⊢ ↑(ofDigits b []) = ofDigits ↑b []
[PROOFSTEP]
rfl
[GOAL]
case cons
n b d : ℕ
L : List ℕ
tail_ih✝ : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(ofDigits b (d :: L)) = ofDigits (↑b) (d :: L)
[PROOFSTEP]
dsimp [ofDigits]
[GOAL]
case cons
n b d : ℕ
L : List ℕ
tail_ih✝ : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(d + b * ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L
[PROOFSTEP]
push_cast
[GOAL]
case cons
n b d : ℕ
L : List ℕ
tail_ih✝ : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ofDigits (↑b) L = ↑d + ↑b * ofDigits (↑b) L
[PROOFSTEP]
simp only
[GOAL]
n b : ℕ
h : 1 < b
L : List ℕ
w₁ : ∀ (l : ℕ), l ∈ L → l < b
w₂ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
⊢ digits b (ofDigits b L) = L
[PROOFSTEP]
induction' L with d L ih
[GOAL]
case nil
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
w₁ : ∀ (l : ℕ), l ∈ [] → l < b
w₂ : ∀ (h : [] ≠ []), List.getLast [] h ≠ 0
⊢ digits b (ofDigits b []) = []
[PROOFSTEP]
dsimp [ofDigits]
[GOAL]
case nil
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
w₁ : ∀ (l : ℕ), l ∈ [] → l < b
w₂ : ∀ (h : [] ≠ []), List.getLast [] h ≠ 0
⊢ digits b 0 = []
[PROOFSTEP]
simp
[GOAL]
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : ∀ (h : d :: L ≠ []), List.getLast (d :: L) h ≠ 0
⊢ digits b (ofDigits b (d :: L)) = d :: L
[PROOFSTEP]
dsimp [ofDigits]
[GOAL]
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : ∀ (h : d :: L ≠ []), List.getLast (d :: L) h ≠ 0
⊢ digits b (d + b * ofDigits b L) = d :: L
[PROOFSTEP]
replace w₂ := w₂ (by simp)
[GOAL]
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : ∀ (h : d :: L ≠ []), List.getLast (d :: L) h ≠ 0
⊢ d :: L ≠ []
[PROOFSTEP]
simp
[GOAL]
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ digits b (d + b * ofDigits b L) = d :: L
[PROOFSTEP]
rw [digits_add b h]
[GOAL]
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ d :: digits b (ofDigits b L) = d :: L
[PROOFSTEP]
rw [ih]
[GOAL]
case cons.w₁
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ ∀ (l : ℕ), l ∈ L → l < b
[PROOFSTEP]
intro l m
[GOAL]
case cons.w₁
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
l : ℕ
m : l ∈ L
⊢ l < b
[PROOFSTEP]
apply w₁
[GOAL]
case cons.w₁.a
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
l : ℕ
m : l ∈ L
⊢ l ∈ d :: L
[PROOFSTEP]
exact List.mem_cons_of_mem _ m
[GOAL]
case cons.w₂
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ ∀ (h : L ≠ []), List.getLast L h ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case cons.w₂
n b : ℕ
h✝ : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h : L ≠ []
⊢ List.getLast L h ≠ 0
[PROOFSTEP]
rw [List.getLast_cons h] at w₂
[GOAL]
case cons.w₂
n b : ℕ
h✝ : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h : L ≠ []
w₂ : List.getLast L h ≠ 0
⊢ List.getLast L h ≠ 0
[PROOFSTEP]
convert w₂
[GOAL]
case cons.hxb
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ d < b
[PROOFSTEP]
exact w₁ d (List.mem_cons_self _ _)
[GOAL]
case cons.hxy
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
[PROOFSTEP]
by_cases h' : L = []
[GOAL]
case pos
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h' : L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
[PROOFSTEP]
rcases h' with rfl
[GOAL]
case pos
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
d : ℕ
ih : (∀ (l : ℕ), l ∈ [] → l < b) → (∀ (h : [] ≠ []), List.getLast [] h ≠ 0) → digits b (ofDigits b []) = []
w₁ : ∀ (l : ℕ), l ∈ [d] → l < b
w₂ : List.getLast [d] (_ : ¬[d] = []) ≠ 0
⊢ d ≠ 0 ∨ ofDigits b [] ≠ 0
[PROOFSTEP]
left
[GOAL]
case pos.h
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
d : ℕ
ih : (∀ (l : ℕ), l ∈ [] → l < b) → (∀ (h : [] ≠ []), List.getLast [] h ≠ 0) → digits b (ofDigits b []) = []
w₁ : ∀ (l : ℕ), l ∈ [d] → l < b
w₂ : List.getLast [d] (_ : ¬[d] = []) ≠ 0
⊢ d ≠ 0
[PROOFSTEP]
simpa using w₂
[GOAL]
case neg
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
[PROOFSTEP]
right
[GOAL]
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h' : ¬L = []
⊢ ofDigits b L ≠ 0
[PROOFSTEP]
contrapose! w₂
[GOAL]
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ List.getLast (d :: L) (_ : ¬d :: L = []) = 0
[PROOFSTEP]
refine' digits_zero_of_eq_zero h.ne_bot w₂ _ _
[GOAL]
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ List.getLast (d :: L) (_ : ¬d :: L = []) ∈ L
[PROOFSTEP]
rw [List.getLast_cons h']
[GOAL]
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ List.getLast L h' ∈ L
[PROOFSTEP]
exact List.getLast_mem h'
[GOAL]
n✝ b n : ℕ
⊢ ofDigits b (digits b n) = n
[PROOFSTEP]
cases' b with b
[GOAL]
case zero
n✝ n : ℕ
⊢ ofDigits zero (digits zero n) = n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero.zero
n : ℕ
⊢ ofDigits zero (digits zero zero) = zero
[PROOFSTEP]
rfl
[GOAL]
case zero.succ
n✝ n : ℕ
⊢ ofDigits zero (digits zero (succ n)) = succ n
[PROOFSTEP]
change ofDigits 0 [n + 1] = n + 1
[GOAL]
case zero.succ
n✝ n : ℕ
⊢ ofDigits 0 [n + 1] = n + 1
[PROOFSTEP]
dsimp [ofDigits]
[GOAL]
case succ
n✝ n b : ℕ
⊢ ofDigits (succ b) (digits (succ b) n) = n
[PROOFSTEP]
cases' b with b
[GOAL]
case succ.zero
n✝ n : ℕ
⊢ ofDigits (succ zero) (digits (succ zero) n) = n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case succ.zero.zero
n : ℕ
⊢ ofDigits (succ zero) (digits (succ zero) zero) = zero
[PROOFSTEP]
rfl
[GOAL]
case succ.zero.succ
n✝ n : ℕ
ih : ofDigits (succ zero) (digits (succ zero) n) = n
⊢ ofDigits (succ zero) (digits (succ zero) (succ n)) = succ n
[PROOFSTEP]
rw [show succ zero = 1 by rfl] at ih ⊢
[GOAL]
n✝ n : ℕ
ih : ofDigits (succ zero) (digits (succ zero) n) = n
⊢ succ zero = 1
[PROOFSTEP]
rfl
[GOAL]
n✝ n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ succ zero = 1
[PROOFSTEP]
rfl
[GOAL]
case succ.zero.succ
n✝ n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ ofDigits 1 (digits 1 (succ n)) = succ n
[PROOFSTEP]
simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
[GOAL]
case succ.succ
n✝ n b : ℕ
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
[PROOFSTEP]
apply Nat.strongInductionOn n _
[GOAL]
n✝ n b : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m) →
      ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
[PROOFSTEP]
clear n
[GOAL]
n b : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m) →
      ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
[PROOFSTEP]
intro n h
[GOAL]
n✝ b n : ℕ
h : ∀ (m : ℕ), m < n → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
[PROOFSTEP]
cases n
[GOAL]
case zero
n b : ℕ
h : ∀ (m : ℕ), m < zero → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) zero) = zero
[PROOFSTEP]
rw [digits_zero]
[GOAL]
case zero
n b : ℕ
h : ∀ (m : ℕ), m < zero → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) [] = zero
[PROOFSTEP]
rfl
[GOAL]
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) (succ n✝)) = succ n✝
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, digits_add_two_add_one]
[GOAL]
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (b + 1 + 1) ((n✝ + 1) % (b + 2) :: digits (b + 2) ((n✝ + 1) / (b + 2))) = n✝ + 1
[PROOFSTEP]
dsimp [ofDigits]
[GOAL]
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ofDigits (b + 1 + 1) (digits (b + 2) ((n✝ + 1) / (b + 2))) = n✝ + 1
[PROOFSTEP]
rw [h _ (Nat.div_lt_self' _ b)]
[GOAL]
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ((n✝ + 1) / (b + 2)) = n✝ + 1
[PROOFSTEP]
rw [Nat.mod_add_div]
[GOAL]
n : ℕ
L : List ℕ
⊢ ofDigits 1 L = List.sum L
[PROOFSTEP]
induction' L with _ _ ih
[GOAL]
case nil
n : ℕ
⊢ ofDigits 1 [] = List.sum []
[PROOFSTEP]
rfl
[GOAL]
case cons
n head✝ : ℕ
tail✝ : List ℕ
ih : ofDigits 1 tail✝ = List.sum tail✝
⊢ ofDigits 1 (head✝ :: tail✝) = List.sum (head✝ :: tail✝)
[PROOFSTEP]
simp [ofDigits, List.sum_cons, ih]
[GOAL]
n✝ b n : ℕ
⊢ digits b n = [] ↔ n = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
n✝ b n : ℕ
⊢ digits b n = [] → n = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
n✝ b n : ℕ
h : digits b n = []
⊢ n = 0
[PROOFSTEP]
have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
[GOAL]
n✝ b n : ℕ
h : digits b n = []
⊢ ofDigits b (digits b n) = ofDigits b []
[PROOFSTEP]
rw [h]
[GOAL]
case mp
n✝ b n : ℕ
h : digits b n = []
this : ofDigits b (digits b n) = ofDigits b []
⊢ n = 0
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2
n✝ b n : ℕ
h : digits b n = []
this : ofDigits b (digits b n) = ofDigits b []
⊢ n = ofDigits b (digits b n)
[PROOFSTEP]
rw [ofDigits_digits]
[GOAL]
case mpr
n✝ b n : ℕ
⊢ n = 0 → digits b n = []
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
n b : ℕ
⊢ digits b 0 = []
[PROOFSTEP]
simp
[GOAL]
n✝ b n : ℕ
h : 1 < b
w : n ≠ 0
⊢ digits b n = n % b :: digits b (n / b)
[PROOFSTEP]
rcases b with (_ | _ | b)
[GOAL]
case zero
n✝ n : ℕ
w : n ≠ 0
h : 1 < zero
⊢ digits zero n = n % zero :: digits zero (n / zero)
[PROOFSTEP]
rw [digits_zero_succ' w, Nat.mod_zero, Nat.div_zero, Nat.digits_zero_zero]
[GOAL]
case succ.zero
n✝ n : ℕ
w : n ≠ 0
h : 1 < succ zero
⊢ digits (succ zero) n = n % succ zero :: digits (succ zero) (n / succ zero)
[PROOFSTEP]
norm_num at h
[GOAL]
case succ.succ
n✝ n : ℕ
w : n ≠ 0
b : ℕ
h : 1 < succ (succ b)
⊢ digits (succ (succ b)) n = n % succ (succ b) :: digits (succ (succ b)) (n / succ (succ b))
[PROOFSTEP]
rcases n with (_ | n)
[GOAL]
case succ.succ.zero
n b : ℕ
h : 1 < succ (succ b)
w : zero ≠ 0
⊢ digits (succ (succ b)) zero = zero % succ (succ b) :: digits (succ (succ b)) (zero / succ (succ b))
[PROOFSTEP]
norm_num at w
[GOAL]
case succ.succ.succ
n✝ b : ℕ
h : 1 < succ (succ b)
n : ℕ
w : succ n ≠ 0
⊢ digits (succ (succ b)) (succ n) = succ n % succ (succ b) :: digits (succ (succ b)) (succ n / succ (succ b))
[PROOFSTEP]
simp only [digits_add_two_add_one, ne_eq]
[GOAL]
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
⊢ List.getLast (digits b m) p = List.getLast (digits b (m / b)) q
[PROOFSTEP]
by_cases hm : m = 0
[GOAL]
case pos
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
hm : m = 0
⊢ List.getLast (digits b m) p = List.getLast (digits b (m / b)) q
[PROOFSTEP]
simp [hm]
[GOAL]
case neg
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
hm : ¬m = 0
⊢ List.getLast (digits b m) p = List.getLast (digits b (m / b)) q
[PROOFSTEP]
simp only [digits_eq_cons_digits_div h hm]
[GOAL]
case neg
n b m : ℕ
h : 1 < b
p : digits b m ≠ []
q : digits b (m / b) ≠ []
hm : ¬m = 0
⊢ List.getLast (m % b :: digits b (m / b)) (_ : m % b :: digits b (m / b) ≠ []) = List.getLast (digits b (m / b)) q
[PROOFSTEP]
rw [List.getLast_cons]
[GOAL]
n✝ b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ List.length (digits b n) = log b n + 1
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n IH
[GOAL]
case h
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
⊢ List.length (digits b n) = log b n + 1
[PROOFSTEP]
rw [digits_eq_cons_digits_div hb hn, List.length]
[GOAL]
case h
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
[PROOFSTEP]
by_cases h : n / b = 0
[GOAL]
case pos
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
[PROOFSTEP]
have hb0 : b ≠ 0 := (Nat.succ_le_iff.1 hb).ne_bot
[GOAL]
case pos
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : n / b = 0
hb0 : b ≠ 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
[PROOFSTEP]
simp [h, log_eq_zero_iff, ← Nat.div_eq_zero_iff hb0.bot_lt]
[GOAL]
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
[PROOFSTEP]
have : n / b < n := div_lt_self (Nat.pos_of_ne_zero hn) hb
[GOAL]
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
[PROOFSTEP]
rw [IH _ this h, log_div_base, tsub_add_cancel_of_le]
[GOAL]
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ 1 ≤ log b n
[PROOFSTEP]
refine' Nat.succ_le_of_lt (log_pos hb _)
[GOAL]
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ b ≤ n
[PROOFSTEP]
contrapose! h
[GOAL]
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
this : n / b < n
h : n < b
⊢ n / b = 0
[PROOFSTEP]
exact div_eq_of_lt h
[GOAL]
n b m : ℕ
hm : m ≠ 0
⊢ List.getLast (digits b m) (_ : digits b m ≠ []) ≠ 0
[PROOFSTEP]
rcases b with (_ | _ | b)
[GOAL]
case zero
n m : ℕ
hm : m ≠ 0
⊢ List.getLast (digits zero m) (_ : digits zero m ≠ []) ≠ 0
[PROOFSTEP]
cases m
[GOAL]
case zero.zero
n : ℕ
hm : zero ≠ 0
⊢ List.getLast (digits zero zero) (_ : digits zero zero ≠ []) ≠ 0
[PROOFSTEP]
cases hm rfl
[GOAL]
case zero.succ
n n✝ : ℕ
hm : succ n✝ ≠ 0
⊢ List.getLast (digits zero (succ n✝)) (_ : digits zero (succ n✝) ≠ []) ≠ 0
[PROOFSTEP]
simp
[GOAL]
case succ.zero
n m : ℕ
hm : m ≠ 0
⊢ List.getLast (digits (succ zero) m) (_ : digits (succ zero) m ≠ []) ≠ 0
[PROOFSTEP]
cases m
[GOAL]
case succ.zero.zero
n : ℕ
hm : zero ≠ 0
⊢ List.getLast (digits (succ zero) zero) (_ : digits (succ zero) zero ≠ []) ≠ 0
[PROOFSTEP]
cases hm rfl
[GOAL]
case succ.zero.succ
n n✝ : ℕ
hm : succ n✝ ≠ 0
⊢ List.getLast (digits (succ zero) (succ n✝)) (_ : digits (succ zero) (succ n✝) ≠ []) ≠ 0
[PROOFSTEP]
rename ℕ => m
[GOAL]
case succ.zero.succ
n m : ℕ
hm : succ m ≠ 0
⊢ List.getLast (digits (succ zero) (succ m)) (_ : digits (succ zero) (succ m) ≠ []) ≠ 0
[PROOFSTEP]
simp only [digits_one, List.getLast_replicate_succ m 1]
[GOAL]
case succ.succ
n m : ℕ
hm : m ≠ 0
b : ℕ
⊢ List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
[PROOFSTEP]
revert hm
[GOAL]
case succ.succ
n m b : ℕ
⊢ ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
[PROOFSTEP]
apply Nat.strongInductionOn m
[GOAL]
case succ.succ
n m b : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0) →
      ∀ (hm : n ≠ 0), List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
[PROOFSTEP]
intro n IH hn
[GOAL]
case succ.succ
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
⊢ List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
[PROOFSTEP]
by_cases hnb : n < b + 2
[GOAL]
case pos
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : n < b + 2
⊢ List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
[PROOFSTEP]
simpa only [digits_of_lt (b + 2) n hn hnb]
[GOAL]
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
[PROOFSTEP]
rw [digits_getLast n (le_add_left 2 b)]
[GOAL]
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ List.getLast (digits (b + 2) (n / (b + 2))) ?neg.q✝ ≠ 0
case neg.q
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ digits (b + 2) (n / (b + 2)) ≠ []
[PROOFSTEP]
refine' IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) _
[GOAL]
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ n / succ (succ b) ≠ 0
[PROOFSTEP]
rw [← pos_iff_ne_zero]
[GOAL]
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ 0 < n / succ (succ b)
[PROOFSTEP]
exact Nat.div_pos (le_of_not_lt hnb) (zero_lt_succ (succ b))
[GOAL]
n b m : ℕ
⊢ ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
[PROOFSTEP]
apply Nat.strongInductionOn m
[GOAL]
n b m : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2) → ∀ {d : ℕ}, d ∈ digits (b + 2) n → d < b + 2
[PROOFSTEP]
intro n IH d hd
[GOAL]
n✝ b m n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
d : ℕ
hd : d ∈ digits (b + 2) n
⊢ d < b + 2
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
n b m d : ℕ
IH : ∀ (m : ℕ), m < zero → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ digits (b + 2) zero
⊢ d < b + 2
[PROOFSTEP]
rw [digits_zero] at hd
[GOAL]
case zero
n b m d : ℕ
IH : ∀ (m : ℕ), m < zero → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ []
⊢ d < b + 2
[PROOFSTEP]
cases hd
[GOAL]
case succ
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ digits (b + 2) (succ n)
⊢ d < b + 2
[PROOFSTEP]
rw [digits_add_two_add_one] at hd
[GOAL]
case succ
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: digits (b + 2) ((n + 1) / (b + 2))
⊢ d < b + 2
[PROOFSTEP]
cases hd
[GOAL]
case succ.head
n✝ b m n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
⊢ (n + 1) % (b + 2) < b + 2
[PROOFSTEP]
exact
  n.succ.mod_lt
    (by simp)
      -- Porting note: Previous code (single line) contained linarith.
        -- . exact IH _ (Nat.div_lt_self (Nat.succ_pos _) (by linarith)) hd
[GOAL]
n✝ b m n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
⊢ b + 2 > 0
[PROOFSTEP]
simp
[GOAL]
case succ.tail
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ d < b + 2
[PROOFSTEP]
apply IH ((n + 1) / (b + 2))
[GOAL]
case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ (n + 1) / (b + 2) < succ n
[PROOFSTEP]
apply Nat.div_lt_self
[GOAL]
case succ.tail.a.hLtN
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ 0 < n + 1
[PROOFSTEP]
simp
[GOAL]
case succ.tail.a.hLtK
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ 1 < b + 2
[PROOFSTEP]
simp
[GOAL]
case succ.tail.a
n✝ b m d n : ℕ
IH : ∀ (m : ℕ), m < succ n → ∀ {d : ℕ}, d ∈ digits (b + 2) m → d < b + 2
a✝ : List.Mem d (digits (b + 2) ((n + 1) / (b + 2)))
⊢ d ∈ digits (b + 2) ((n + 1) / (b + 2))
[PROOFSTEP]
assumption
[GOAL]
n b m d : ℕ
hb : 1 < b
hd : d ∈ digits b m
⊢ d < b
[PROOFSTEP]
rcases b with (_ | _ | b)
[GOAL]
case zero
n m d : ℕ
hb : 1 < zero
hd : d ∈ digits zero m
⊢ d < zero
[PROOFSTEP]
try simp_all
[GOAL]
case zero
n m d : ℕ
hb : 1 < zero
hd : d ∈ digits zero m
⊢ d < zero
[PROOFSTEP]
simp_all
[GOAL]
case succ.zero
n m d : ℕ
hb : 1 < succ zero
hd : d ∈ digits (succ zero) m
⊢ d < succ zero
[PROOFSTEP]
try simp_all
[GOAL]
case succ.zero
n m d : ℕ
hb : 1 < succ zero
hd : d ∈ digits (succ zero) m
⊢ d < succ zero
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
n m d b : ℕ
hb : 1 < succ (succ b)
hd : d ∈ digits (succ (succ b)) m
⊢ d < succ (succ b)
[PROOFSTEP]
try simp_all
[GOAL]
case succ.succ
n m d b : ℕ
hb : 1 < succ (succ b)
hd : d ∈ digits (succ (succ b)) m
⊢ d < succ (succ b)
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
n m d b : ℕ
hd : d ∈ digits (succ (succ b)) m
⊢ d < succ (succ b)
[PROOFSTEP]
exact digits_lt_base' hd
[GOAL]
n b : ℕ
l : List ℕ
hl : ∀ (x : ℕ), x ∈ l → x < b + 2
⊢ ofDigits (b + 2) l < (b + 2) ^ List.length l
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
n b : ℕ
l : List ℕ
hl✝ : ∀ (x : ℕ), x ∈ l → x < b + 2
hl : ∀ (x : ℕ), x ∈ [] → x < b + 2
⊢ ofDigits (b + 2) [] < (b + 2) ^ List.length []
[PROOFSTEP]
simp [ofDigits]
[GOAL]
case cons
n b : ℕ
l : List ℕ
hl✝ : ∀ (x : ℕ), x ∈ l → x < b + 2
hd : ℕ
tl : List ℕ
IH : (∀ (x : ℕ), x ∈ tl → x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ List.length tl
hl : ∀ (x : ℕ), x ∈ hd :: tl → x < b + 2
⊢ ofDigits (b + 2) (hd :: tl) < (b + 2) ^ List.length (hd :: tl)
[PROOFSTEP]
rw [ofDigits, List.length_cons, pow_succ]
[GOAL]
case cons
n b : ℕ
l : List ℕ
hl✝ : ∀ (x : ℕ), x ∈ l → x < b + 2
hd : ℕ
tl : List ℕ
IH : (∀ (x : ℕ), x ∈ tl → x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ List.length tl
hl : ∀ (x : ℕ), x ∈ hd :: tl → x < b + 2
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ List.length tl * (b + 2)
[PROOFSTEP]
have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
  mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le]) (Nat.zero_le _)
[GOAL]
n b : ℕ
l : List ℕ
hl✝ : ∀ (x : ℕ), x ∈ l → x < b + 2
hd : ℕ
tl : List ℕ
IH : (∀ (x : ℕ), x ∈ tl → x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ List.length tl
hl : ∀ (x : ℕ), x ∈ hd :: tl → x < b + 2
⊢ b + 2 ≤ b + 2
[PROOFSTEP]
rfl
[GOAL]
n b : ℕ
l : List ℕ
hl✝ : ∀ (x : ℕ), x ∈ l → x < b + 2
hd : ℕ
tl : List ℕ
IH : (∀ (x : ℕ), x ∈ tl → x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ List.length tl
hl : ∀ (x : ℕ), x ∈ hd :: tl → x < b + 2
⊢ 0 ≤ b + 2
[PROOFSTEP]
simp only [zero_le]
[GOAL]
case cons
n b : ℕ
l : List ℕ
hl✝ : ∀ (x : ℕ), x ∈ l → x < b + 2
hd : ℕ
tl : List ℕ
IH : (∀ (x : ℕ), x ∈ tl → x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ List.length tl
hl : ∀ (x : ℕ), x ∈ hd :: tl → x < b + 2
this : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ List.length tl * (b + 2)
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ List.length tl * (b + 2)
[PROOFSTEP]
suffices ↑hd < b + 2 by linarith
[GOAL]
n b : ℕ
l : List ℕ
hl✝ : ∀ (x : ℕ), x ∈ l → x < b + 2
hd : ℕ
tl : List ℕ
IH : (∀ (x : ℕ), x ∈ tl → x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ List.length tl
hl : ∀ (x : ℕ), x ∈ hd :: tl → x < b + 2
this✝ : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ List.length tl * (b + 2)
this : hd < b + 2
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ List.length tl * (b + 2)
[PROOFSTEP]
linarith
[GOAL]
case cons
n b : ℕ
l : List ℕ
hl✝ : ∀ (x : ℕ), x ∈ l → x < b + 2
hd : ℕ
tl : List ℕ
IH : (∀ (x : ℕ), x ∈ tl → x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ List.length tl
hl : ∀ (x : ℕ), x ∈ hd :: tl → x < b + 2
this : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ List.length tl * (b + 2)
⊢ hd < b + 2
[PROOFSTEP]
norm_cast
[GOAL]
case cons
n b : ℕ
l : List ℕ
hl✝ : ∀ (x : ℕ), x ∈ l → x < b + 2
hd : ℕ
tl : List ℕ
IH : (∀ (x : ℕ), x ∈ tl → x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ List.length tl
hl : ∀ (x : ℕ), x ∈ hd :: tl → x < b + 2
this : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ List.length tl * (b + 2)
⊢ hd < b + 2
[PROOFSTEP]
exact hl hd (List.mem_cons_self _ _)
[GOAL]
n b : ℕ
l : List ℕ
hb : 1 < b
hl : ∀ (x : ℕ), x ∈ l → x < b
⊢ ofDigits b l < b ^ List.length l
[PROOFSTEP]
rcases b with (_ | _ | b)
[GOAL]
case zero
n : ℕ
l : List ℕ
hb : 1 < zero
hl : ∀ (x : ℕ), x ∈ l → x < zero
⊢ ofDigits zero l < zero ^ List.length l
[PROOFSTEP]
try simp_all
[GOAL]
case zero
n : ℕ
l : List ℕ
hb : 1 < zero
hl : ∀ (x : ℕ), x ∈ l → x < zero
⊢ ofDigits zero l < zero ^ List.length l
[PROOFSTEP]
simp_all
[GOAL]
case succ.zero
n : ℕ
l : List ℕ
hb : 1 < succ zero
hl : ∀ (x : ℕ), x ∈ l → x < succ zero
⊢ ofDigits (succ zero) l < succ zero ^ List.length l
[PROOFSTEP]
try simp_all
[GOAL]
case succ.zero
n : ℕ
l : List ℕ
hb : 1 < succ zero
hl : ∀ (x : ℕ), x ∈ l → x < succ zero
⊢ ofDigits (succ zero) l < succ zero ^ List.length l
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
n : ℕ
l : List ℕ
b : ℕ
hb : 1 < succ (succ b)
hl : ∀ (x : ℕ), x ∈ l → x < succ (succ b)
⊢ ofDigits (succ (succ b)) l < succ (succ b) ^ List.length l
[PROOFSTEP]
try simp_all
[GOAL]
case succ.succ
n : ℕ
l : List ℕ
b : ℕ
hb : 1 < succ (succ b)
hl : ∀ (x : ℕ), x ∈ l → x < succ (succ b)
⊢ ofDigits (succ (succ b)) l < succ (succ b) ^ List.length l
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
n : ℕ
l : List ℕ
b : ℕ
hl : ∀ (x : ℕ), x ∈ l → x < succ (succ b)
⊢ ofDigits (succ (succ b)) l < succ (succ b) ^ List.length l
[PROOFSTEP]
exact ofDigits_lt_base_pow_length' hl
[GOAL]
n b m : ℕ
⊢ m < (b + 2) ^ List.length (digits (b + 2) m)
[PROOFSTEP]
convert @ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'
[GOAL]
case h.e'_3
n b m : ℕ
⊢ m = ofDigits (b + 2) (digits (b + 2) m)
[PROOFSTEP]
rw [ofDigits_digits (b + 2) m]
[GOAL]
n b m : ℕ
hb : 1 < b
⊢ m < b ^ List.length (digits b m)
[PROOFSTEP]
rcases b with (_ | _ | b)
[GOAL]
case zero
n m : ℕ
hb : 1 < zero
⊢ m < zero ^ List.length (digits zero m)
[PROOFSTEP]
try simp_all
[GOAL]
case zero
n m : ℕ
hb : 1 < zero
⊢ m < zero ^ List.length (digits zero m)
[PROOFSTEP]
simp_all
[GOAL]
case succ.zero
n m : ℕ
hb : 1 < succ zero
⊢ m < succ zero ^ List.length (digits (succ zero) m)
[PROOFSTEP]
try simp_all
[GOAL]
case succ.zero
n m : ℕ
hb : 1 < succ zero
⊢ m < succ zero ^ List.length (digits (succ zero) m)
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
n m b : ℕ
hb : 1 < succ (succ b)
⊢ m < succ (succ b) ^ List.length (digits (succ (succ b)) m)
[PROOFSTEP]
try simp_all
[GOAL]
case succ.succ
n m b : ℕ
hb : 1 < succ (succ b)
⊢ m < succ (succ b) ^ List.length (digits (succ (succ b)) m)
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
n m b : ℕ
⊢ m < succ (succ b) ^ List.length (digits (succ (succ b)) m)
[PROOFSTEP]
exact lt_base_pow_length_digits'
[GOAL]
n✝ b m n : ℕ
⊢ ofDigits b (digits b n ++ digits b m) = n + b ^ List.length (digits b n) * m
[PROOFSTEP]
rw [ofDigits_append, ofDigits_digits, ofDigits_digits]
[GOAL]
n✝ b n : ℕ
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
[PROOFSTEP]
rcases Decidable.eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
n b : ℕ
⊢ List.length (digits b 0) ≤ List.length (digits b (0 + 1))
[PROOFSTEP]
simp
[GOAL]
case inr
n✝ b n : ℕ
hn : n ≠ 0
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inr.inl
n✝ b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
[PROOFSTEP]
interval_cases b
[GOAL]
case inr.inl.«0»
n✝ b n : ℕ
hn : n ≠ 0
hb : 0 ≤ 1
⊢ List.length (digits 0 n) ≤ List.length (digits 0 (n + 1))
[PROOFSTEP]
simp_arith [digits_zero_succ', hn]
[GOAL]
case inr.inl.«1»
n✝ b n : ℕ
hn : n ≠ 0
hb : 1 ≤ 1
⊢ List.length (digits 1 n) ≤ List.length (digits 1 (n + 1))
[PROOFSTEP]
simp_arith [digits_zero_succ', hn]
[GOAL]
case inr.inr
n✝ b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ List.length (digits b n) ≤ List.length (digits b (n + 1))
[PROOFSTEP]
simpa [digits_len, hb, hn] using log_mono_right (le_succ _)
[GOAL]
n p q : ℕ
L : List ℕ
h : p ≤ q
⊢ ofDigits p L ≤ ofDigits q L
[PROOFSTEP]
induction' L with _ _ hi
[GOAL]
case nil
n p q : ℕ
h : p ≤ q
⊢ ofDigits p [] ≤ ofDigits q []
[PROOFSTEP]
rfl
[GOAL]
case cons
n p q : ℕ
h : p ≤ q
head✝ : ℕ
tail✝ : List ℕ
hi : ofDigits p tail✝ ≤ ofDigits q tail✝
⊢ ofDigits p (head✝ :: tail✝) ≤ ofDigits q (head✝ :: tail✝)
[PROOFSTEP]
simp only [ofDigits, cast_id, add_le_add_iff_left]
[GOAL]
case cons
n p q : ℕ
h : p ≤ q
head✝ : ℕ
tail✝ : List ℕ
hi : ofDigits p tail✝ ≤ ofDigits q tail✝
⊢ p * ofDigits p tail✝ ≤ q * ofDigits q tail✝
[PROOFSTEP]
exact Nat.mul_le_mul h hi
[GOAL]
n✝ p n : ℕ
⊢ List.sum (digits p n) ≤ n
[PROOFSTEP]
induction' n with n
[GOAL]
case zero
n p : ℕ
⊢ List.sum (digits p zero) ≤ zero
[PROOFSTEP]
exact digits_zero _ ▸ Nat.le_refl (List.sum [])
[GOAL]
case succ
n✝ p n : ℕ
n_ih✝ : List.sum (digits p n) ≤ n
⊢ List.sum (digits p (succ n)) ≤ succ n
[PROOFSTEP]
induction' p with p
[GOAL]
case succ.zero
n✝ p n : ℕ
n_ih✝¹ : List.sum (digits p n) ≤ n
n_ih✝ : List.sum (digits zero n) ≤ n
⊢ List.sum (digits zero (succ n)) ≤ succ n
[PROOFSTEP]
rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
[GOAL]
case succ.succ
n✝ p✝ n : ℕ
n_ih✝² : List.sum (digits p✝ n) ≤ n
p : ℕ
n_ih✝¹ : List.sum (digits p n) ≤ n → List.sum (digits p (succ n)) ≤ succ n
n_ih✝ : List.sum (digits (succ p) n) ≤ n
⊢ List.sum (digits (succ p) (succ n)) ≤ succ n
[PROOFSTEP]
nth_rw 2 [← ofDigits_digits p.succ n.succ]
[GOAL]
case succ.succ
n✝ p✝ n : ℕ
n_ih✝² : List.sum (digits p✝ n) ≤ n
p : ℕ
n_ih✝¹ : List.sum (digits p n) ≤ n → List.sum (digits p (succ n)) ≤ succ n
n_ih✝ : List.sum (digits (succ p) n) ≤ n
⊢ List.sum (digits (succ p) (succ n)) ≤ ofDigits (succ p) (digits (succ p) (succ n))
[PROOFSTEP]
rw [← ofDigits_one <| digits p.succ n.succ]
[GOAL]
case succ.succ
n✝ p✝ n : ℕ
n_ih✝² : List.sum (digits p✝ n) ≤ n
p : ℕ
n_ih✝¹ : List.sum (digits p n) ≤ n → List.sum (digits p (succ n)) ≤ succ n
n_ih✝ : List.sum (digits (succ p) n) ≤ n
⊢ ofDigits 1 (digits (succ p) (succ n)) ≤ ofDigits (succ p) (digits (succ p) (succ n))
[PROOFSTEP]
exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p
[GOAL]
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
⊢ (b + 2) ^ List.length l ≤ (b + 2) * ofDigits (b + 2) l
[PROOFSTEP]
rw [← List.dropLast_append_getLast hl]
[GOAL]
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
⊢ (b + 2) ^ List.length (List.dropLast l ++ [List.getLast l hl]) ≤
    (b + 2) * ofDigits (b + 2) (List.dropLast l ++ [List.getLast l hl])
[PROOFSTEP]
simp only [List.length_append, List.length, zero_add, List.length_dropLast, ofDigits_append, List.length_dropLast,
  ofDigits_singleton, add_comm (l.length - 1), pow_add, pow_one]
[GOAL]
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
⊢ (b + 2) * (b + 2) ^ (List.length l - 1) ≤
    (b + 2) * (ofDigits (b + 2) (List.dropLast l) + (b + 2) ^ (List.length l - 1) * List.getLast l hl)
[PROOFSTEP]
apply Nat.mul_le_mul_left
[GOAL]
case h
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
⊢ (b + 2) ^ (List.length l - 1) ≤ ofDigits (b + 2) (List.dropLast l) + (b + 2) ^ (List.length l - 1) * List.getLast l hl
[PROOFSTEP]
refine' le_trans _ (Nat.le_add_left _ _)
[GOAL]
case h
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
⊢ (b + 2) ^ (List.length l - 1) ≤ (b + 2) ^ (List.length l - 1) * List.getLast l hl
[PROOFSTEP]
have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]
[GOAL]
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
⊢ 0 < List.getLast l hl
[PROOFSTEP]
rwa [pos_iff_ne_zero]
[GOAL]
case h
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
this : 0 < List.getLast l hl
⊢ (b + 2) ^ (List.length l - 1) ≤ (b + 2) ^ (List.length l - 1) * List.getLast l hl
[PROOFSTEP]
convert Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1
[GOAL]
case h.e'_3
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
this : 0 < List.getLast l hl
⊢ (b + 2) ^ (List.length l - 1) = (b + 2) ^ (List.length l - 1) * succ 0
[PROOFSTEP]
rw [Nat.mul_one]
[GOAL]
n b m : ℕ
hm : m ≠ 0
⊢ (b + 2) ^ List.length (digits (b + 2) m) ≤ (b + 2) * m
[PROOFSTEP]
have : digits (b + 2) m ≠ [] := digits_ne_nil_iff_ne_zero.mpr hm
[GOAL]
n b m : ℕ
hm : m ≠ 0
this : digits (b + 2) m ≠ []
⊢ (b + 2) ^ List.length (digits (b + 2) m) ≤ (b + 2) * m
[PROOFSTEP]
convert @pow_length_le_mul_ofDigits b (digits (b + 2) m) this (getLast_digit_ne_zero _ hm)
[GOAL]
case h.e'_4.h.e'_6
n b m : ℕ
hm : m ≠ 0
this : digits (b + 2) m ≠ []
⊢ m = ofDigits (b + 2) (digits (b + 2) m)
[PROOFSTEP]
rw [ofDigits_digits]
[GOAL]
n b m : ℕ
hb : 1 < b
⊢ m ≠ 0 → b ^ List.length (digits b m) ≤ b * m
[PROOFSTEP]
rcases b with (_ | _ | b)
[GOAL]
case zero
n m : ℕ
hb : 1 < zero
⊢ m ≠ 0 → zero ^ List.length (digits zero m) ≤ zero * m
[PROOFSTEP]
try simp_all
[GOAL]
case zero
n m : ℕ
hb : 1 < zero
⊢ m ≠ 0 → zero ^ List.length (digits zero m) ≤ zero * m
[PROOFSTEP]
simp_all
[GOAL]
case succ.zero
n m : ℕ
hb : 1 < succ zero
⊢ m ≠ 0 → succ zero ^ List.length (digits (succ zero) m) ≤ succ zero * m
[PROOFSTEP]
try simp_all
[GOAL]
case succ.zero
n m : ℕ
hb : 1 < succ zero
⊢ m ≠ 0 → succ zero ^ List.length (digits (succ zero) m) ≤ succ zero * m
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
n m b : ℕ
hb : 1 < succ (succ b)
⊢ m ≠ 0 → succ (succ b) ^ List.length (digits (succ (succ b)) m) ≤ succ (succ b) * m
[PROOFSTEP]
try simp_all
[GOAL]
case succ.succ
n m b : ℕ
hb : 1 < succ (succ b)
⊢ m ≠ 0 → succ (succ b) ^ List.length (digits (succ (succ b)) m) ≤ succ (succ b) * m
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
n m b : ℕ
⊢ ¬m = 0 → succ (succ b) ^ List.length (digits (succ (succ b)) m) ≤ succ (succ b) * m
[PROOFSTEP]
exact base_pow_length_digits_le' b m
[GOAL]
n p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ (l : ℕ), l ∈ digits → l < p
⊢ ofDigits p digits / p = ofDigits p (List.tail digits)
[PROOFSTEP]
induction' digits with hd tl
[GOAL]
case nil
n p : ℕ
hpos : 0 < p
digits : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ digits → l < p
w₁ : ∀ (l : ℕ), l ∈ [] → l < p
⊢ ofDigits p [] / p = ofDigits p (List.tail [])
[PROOFSTEP]
simp [ofDigits]
[GOAL]
case cons
n p : ℕ
hpos : 0 < p
digits : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ digits → l < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ (l : ℕ), l ∈ tl → l < p) → ofDigits p tl / p = ofDigits p (List.tail tl)
w₁ : ∀ (l : ℕ), l ∈ hd :: tl → l < p
⊢ ofDigits p (hd :: tl) / p = ofDigits p (List.tail (hd :: tl))
[PROOFSTEP]
refine' Eq.trans (add_mul_div_left hd _ hpos) _
[GOAL]
case cons
n p : ℕ
hpos : 0 < p
digits : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ digits → l < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ (l : ℕ), l ∈ tl → l < p) → ofDigits p tl / p = ofDigits p (List.tail tl)
w₁ : ∀ (l : ℕ), l ∈ hd :: tl → l < p
⊢ hd / p + ofDigits p tl = ofDigits p (List.tail (hd :: tl))
[PROOFSTEP]
rw [Nat.div_eq_zero <| w₁ _ <| List.mem_cons_self _ _, zero_add]
[GOAL]
case cons
n p : ℕ
hpos : 0 < p
digits : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ digits → l < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ (l : ℕ), l ∈ tl → l < p) → ofDigits p tl / p = ofDigits p (List.tail tl)
w₁ : ∀ (l : ℕ), l ∈ hd :: tl → l < p
⊢ ofDigits p tl = ofDigits p (List.tail (hd :: tl))
[PROOFSTEP]
rfl
[GOAL]
n p i : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ (l : ℕ), l ∈ digits → l < p
⊢ ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
[PROOFSTEP]
induction' i with i hi
[GOAL]
case zero
n p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ (l : ℕ), l ∈ digits → l < p
⊢ ofDigits p digits / p ^ zero = ofDigits p (List.drop zero digits)
[PROOFSTEP]
simp
[GOAL]
case succ
n p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ (l : ℕ), l ∈ digits → l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p digits / p ^ succ i = ofDigits p (List.drop (succ i) digits)
[PROOFSTEP]
rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi,
  ofDigits_div_eq_ofDigits_tail hpos (List.drop i digits) <| fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ←
  List.drop_one, List.drop_drop, add_comm]
[GOAL]
n✝ p i n : ℕ
h : 2 ≤ p
⊢ n / p ^ i = ofDigits p (List.drop i (digits p n))
[PROOFSTEP]
convert ofDigits_div_pow_eq_ofDigits_drop i (zero_lt_of_lt h) (p.digits n) (fun l hl ↦ digits_lt_base h hl)
[GOAL]
case h.e'_2.h.e'_5
n✝ p i n : ℕ
h : 2 ≤ p
⊢ n = ofDigits p (digits p n)
[PROOFSTEP]
exact (ofDigits_digits p n).symm
[GOAL]
n p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : List.getLast L h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ L → l < p
⊢ (p - 1) * ∑ i in range (List.length L), ofDigits p L / p ^ succ i = ofDigits p L - List.sum L
[PROOFSTEP]
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
[GOAL]
case inl
n p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : List.getLast L h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
⊢ (p - 1) * ∑ i in range (List.length L), ofDigits p L / p ^ succ i = ofDigits p L - List.sum L
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case inl.nil
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
h_nonempty : [] ≠ []
h_ne_zero : List.getLast [] h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ [] → l < p
⊢ (p - 1) * ∑ i in range (List.length []), ofDigits p [] / p ^ succ i = ofDigits p [] - List.sum []
[PROOFSTEP]
simp [ofDigits]
[GOAL]
case inl.cons
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
⊢ (p - 1) * ∑ i in range (List.length (hd :: tl)), ofDigits p (hd :: tl) / p ^ succ i =
    ofDigits p (hd :: tl) - List.sum (hd :: tl)
[PROOFSTEP]
simp only [List.length_cons, List.sum_cons, self_div_pow_eq_ofDigits_drop _ _ h,
  digits_ofDigits p h (hd :: tl) h_lt (fun _ => h_ne_zero)]
[GOAL]
case inl.cons
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
⊢ (p - 1) * ∑ x in range (succ (List.length tl)), ofDigits p (List.drop (succ x) (hd :: tl)) =
    ofDigits p (hd :: tl) - (hd + List.sum tl)
[PROOFSTEP]
simp only [ofDigits]
[GOAL]
case inl.cons
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
⊢ (p - 1) * ∑ x in range (succ (List.length tl)), ofDigits p (List.drop (succ x) (hd :: tl)) =
    ↑hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
rw [sum_range_succ, Nat.cast_id]
[GOAL]
case inl.cons
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
⊢ (p - 1) *
      (∑ x in range (List.length tl), ofDigits p (List.drop (succ x) (hd :: tl)) +
        ofDigits p (List.drop (succ (List.length tl)) (hd :: tl))) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
simp only [List.drop, List.drop_length]
[GOAL]
case inl.cons
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
⊢ (p - 1) * (∑ x in range (List.length tl), ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
obtain rfl | h' := em <| tl = []
[GOAL]
case inl.cons.inl
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
ih :
  ∀ {h_nonempty : [] ≠ []},
    List.getLast [] h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ [] → l < p) →
        (p - 1) * ∑ i in range (List.length []), ofDigits p [] / p ^ succ i = ofDigits p [] - List.sum []
h_nonempty : [hd] ≠ []
h_ne_zero : List.getLast [hd] h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ [hd] → l < p
⊢ (p - 1) * (∑ x in range (List.length []), ofDigits p (List.drop x []) + ofDigits p []) =
    hd + p * ofDigits p [] - (hd + List.sum [])
[PROOFSTEP]
simp [ofDigits]
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
⊢ (p - 1) * (∑ x in range (List.length tl), ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
w₁' : ∀ (l : ℕ), l ∈ tl → l < p
⊢ (p - 1) * (∑ x in range (List.length tl), ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
w₁' : ∀ (l : ℕ), l ∈ tl → l < p
w₂' : ∀ (h : tl ≠ []), List.getLast tl h ≠ 0
⊢ (p - 1) * (∑ x in range (List.length tl), ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
have ih := ih (w₂' h') w₁'
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
w₁' : ∀ (l : ℕ), l ∈ tl → l < p
w₂' : ∀ (h : tl ≠ []), List.getLast tl h ≠ 0
ih : (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
⊢ (p - 1) * (∑ x in range (List.length tl), ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂', succ_eq_one_add] at ih
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
w₁' : ∀ (l : ℕ), l ∈ tl → l < p
w₂' : ∀ (h : tl ≠ []), List.getLast tl h ≠ 0
ih : (p - 1) * ∑ x in range (List.length tl), ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - List.sum tl
⊢ (p - 1) * (∑ x in range (List.length tl), ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
have := @sum_singleton _ _ tl.length (fun x => ofDigits p <| tl.drop x) _
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
w₁' : ∀ (l : ℕ), l ∈ tl → l < p
w₂' : ∀ (h : tl ≠ []), List.getLast tl h ≠ 0
ih : (p - 1) * ∑ x in range (List.length tl), ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - List.sum tl
this : ∑ x in {List.length tl}, ofDigits p (List.drop x tl) = ofDigits p (List.drop (List.length tl) tl)
⊢ (p - 1) * (∑ x in range (List.length tl), ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
w₁' : ∀ (l : ℕ), l ∈ tl → l < p
w₂' : ∀ (h : tl ≠ []), List.getLast tl h ≠ 0
ih : (p - 1) * ∑ x in range (List.length tl), ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - List.sum tl
this : ∑ x in Ico (List.length tl) (List.length tl + 1), ofDigits p (List.drop x tl) = 0
⊢ (p - 1) * (∑ x in range (List.length tl), ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
have h₁ : 1 ≤ tl.length := List.length_pos.mpr h'
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
w₁' : ∀ (l : ℕ), l ∈ tl → l < p
w₂' : ∀ (h : tl ≠ []), List.getLast tl h ≠ 0
ih : (p - 1) * ∑ x in range (List.length tl), ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - List.sum tl
this : ∑ x in Ico (List.length tl) (List.length tl + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ List.length tl
⊢ (p - 1) * (∑ x in range (List.length tl), ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x in Ico _ _, ofDigits p (tl.drop x)), ← this,
  sum_Ico_consecutive _ h₁ <| le_succ tl.length, ← sum_Ico_add _ 0 tl.length 1, Ico_zero_eq_range, mul_add, mul_add, ih,
  range_one, sum_singleton, List.drop, ofDigits, mul_zero, add_zero, ←
  Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
w₁' : ∀ (l : ℕ), l ∈ tl → l < p
w₂' : ∀ (h : tl ≠ []), List.getLast tl h ≠ 0
ih : (p - 1) * ∑ x in range (List.length tl), ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - List.sum tl
this : ∑ x in Ico (List.length tl) (List.length tl + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ List.length tl
⊢ (p - 1) * ofDigits p tl + ofDigits p tl - List.sum tl = hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
nth_rw 2 [← one_mul <| ofDigits p tl]
[GOAL]
case inl.cons.inr
n p : ℕ
L : List ℕ
h_nonempty✝ : L ≠ []
h_ne_zero✝ : List.getLast L h_nonempty✝ ≠ 0
h_lt✝ : ∀ (l : ℕ), l ∈ L → l < p
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    List.getLast tl h_nonempty ≠ 0 →
      (∀ (l : ℕ), l ∈ tl → l < p) →
        (p - 1) * ∑ i in range (List.length tl), ofDigits p tl / p ^ succ i = ofDigits p tl - List.sum tl
h_nonempty : hd :: tl ≠ []
h_ne_zero : List.getLast (hd :: tl) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ hd :: tl → l < p
h' : ¬tl = []
w₁' : ∀ (l : ℕ), l ∈ tl → l < p
w₂' : ∀ (h : tl ≠ []), List.getLast tl h ≠ 0
ih : (p - 1) * ∑ x in range (List.length tl), ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - List.sum tl
this : ∑ x in Ico (List.length tl) (List.length tl + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ List.length tl
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - List.sum tl = hd + p * ofDigits p tl - (hd + List.sum tl)
[PROOFSTEP]
rw [← add_mul, one_eq_succ_zero, Nat.sub_add_cancel <| zero_lt_of_lt h, Nat.add_sub_add_left]
[GOAL]
case inr.inl
n : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : List.getLast L h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ L → l < 1
⊢ (1 - 1) * ∑ i in range (List.length L), ofDigits 1 L / 1 ^ succ i = ofDigits 1 L - List.sum L
[PROOFSTEP]
simp [ofDigits_one]
[GOAL]
case inr.inr
n p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : List.getLast L h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ L → l < p
h : p < 1
⊢ (p - 1) * ∑ i in range (List.length L), ofDigits p L / p ^ succ i = ofDigits p L - List.sum L
[PROOFSTEP]
simp [lt_one_iff.mp h]
[GOAL]
case inr.inr
n p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : List.getLast L h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ L → l < p
h : p < 1
⊢ 0 = ofDigits 0 L - List.sum L
[PROOFSTEP]
cases L
[GOAL]
case inr.inr.nil
n p : ℕ
h : p < 1
h_nonempty : [] ≠ []
h_ne_zero : List.getLast [] h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ [] → l < p
⊢ 0 = ofDigits 0 [] - List.sum []
[PROOFSTEP]
simp
[GOAL]
case inr.inr.cons
n p : ℕ
h : p < 1
head✝ : ℕ
tail✝ : List ℕ
h_nonempty : head✝ :: tail✝ ≠ []
h_ne_zero : List.getLast (head✝ :: tail✝) h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), l ∈ head✝ :: tail✝ → l < p
⊢ 0 = ofDigits 0 (head✝ :: tail✝) - List.sum (head✝ :: tail✝)
[PROOFSTEP]
simp [ofDigits]
[GOAL]
n✝ p n : ℕ
⊢ (p - 1) * ∑ i in range (succ (log p n)), n / p ^ succ i = n - List.sum (digits p n)
[PROOFSTEP]
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
[GOAL]
case inl
n✝ p n : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i in range (succ (log p n)), n / p ^ succ i = n - List.sum (digits p n)
[PROOFSTEP]
rcases eq_or_ne n 0 with rfl | hn
[GOAL]
case inl.inl
n p : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i in range (succ (log p 0)), 0 / p ^ succ i = 0 - List.sum (digits p 0)
[PROOFSTEP]
simp
[GOAL]
case inl.inr
n✝ p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (p - 1) * ∑ i in range (succ (log p n)), n / p ^ succ i = n - List.sum (digits p n)
[PROOFSTEP]
convert
  sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <| (fun l a ↦ digits_lt_base h a)
[GOAL]
case h.e'_2.h.e'_6.h.h.e'_1
n✝ p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ succ (log p n) = List.length (digits p n)
[PROOFSTEP]
refine' (digits_len p n h hn).symm
[GOAL]
case h.e'_2.h.e'_6.a.h.e'_5
n✝ p n : ℕ
h : 1 < p
hn : n ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range (List.length (digits p n))
⊢ n = ofDigits p (digits p n)
case h.e'_3.h.e'_5 n✝ p n : ℕ h : 1 < p hn : n ≠ 0 ⊢ n = ofDigits p (digits p n)
[PROOFSTEP]
all_goals exact (ofDigits_digits p n).symm
[GOAL]
case h.e'_2.h.e'_6.a.h.e'_5
n✝ p n : ℕ
h : 1 < p
hn : n ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range (List.length (digits p n))
⊢ n = ofDigits p (digits p n)
[PROOFSTEP]
exact (ofDigits_digits p n).symm
[GOAL]
case h.e'_3.h.e'_5
n✝ p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (digits p n)
[PROOFSTEP]
exact (ofDigits_digits p n).symm
[GOAL]
case inr.inl
n✝ n : ℕ
⊢ (1 - 1) * ∑ i in range (succ (log 1 n)), n / 1 ^ succ i = n - List.sum (digits 1 n)
[PROOFSTEP]
simp
[GOAL]
case inr.inr
n✝ p n : ℕ
h : p < 1
⊢ (p - 1) * ∑ i in range (succ (log p n)), n / p ^ succ i = n - List.sum (digits p n)
[PROOFSTEP]
simp [lt_one_iff.mp h]
[GOAL]
case inr.inr
n✝ p n : ℕ
h : p < 1
⊢ 0 = n - List.sum (digits 0 n)
[PROOFSTEP]
cases n
[GOAL]
case inr.inr.zero
n p : ℕ
h : p < 1
⊢ 0 = zero - List.sum (digits 0 zero)
case inr.inr.succ n p : ℕ h : p < 1 n✝ : ℕ ⊢ 0 = succ n✝ - List.sum (digits 0 (succ n✝))
[PROOFSTEP]
all_goals simp
[GOAL]
case inr.inr.zero
n p : ℕ
h : p < 1
⊢ 0 = zero - List.sum (digits 0 zero)
[PROOFSTEP]
simp
[GOAL]
case inr.inr.succ
n p : ℕ
h : p < 1
n✝ : ℕ
⊢ 0 = succ n✝ - List.sum (digits 0 (succ n✝))
[PROOFSTEP]
simp
[GOAL]
n✝ n : ℕ
⊢ digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
[PROOFSTEP]
induction' n using Nat.binaryRecFromOne with b n h ih
[GOAL]
case z₀
n : ℕ
⊢ digits 2 0 = List.map (fun b => bif b then 1 else 0) (bits 0)
[PROOFSTEP]
simp
[GOAL]
case z₁
n : ℕ
⊢ digits 2 1 = List.map (fun b => bif b then 1 else 0) (bits 1)
[PROOFSTEP]
simp
[GOAL]
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (bits (bit b n))
[PROOFSTEP]
rw [bits_append_bit _ _ fun hn => absurd hn h]
[GOAL]
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (b :: bits n)
[PROOFSTEP]
cases b
[GOAL]
case f.false
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit false n) = List.map (fun b => bif b then 1 else 0) (false :: bits n)
[PROOFSTEP]
rw [digits_def' one_lt_two]
[GOAL]
case f.false
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ bit false n % 2 :: digits 2 (bit false n / 2) = List.map (fun b => bif b then 1 else 0) (false :: bits n)
[PROOFSTEP]
simpa [Nat.bit, Nat.bit0_val n]
[GOAL]
case f.false
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ 0 < bit false n
[PROOFSTEP]
simpa [pos_iff_ne_zero, bit_eq_zero_iff]
[GOAL]
case f.true
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit true n) = List.map (fun b => bif b then 1 else 0) (true :: bits n)
[PROOFSTEP]
simpa [Nat.bit, Nat.bit1_val n, add_comm, digits_add 2 one_lt_two 1 n]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
L : List ℕ
⊢ k ∣ ofDigits a L - ofDigits b L
[PROOFSTEP]
induction' L with d L ih
[GOAL]
case nil
n : ℕ
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ ofDigits a [] - ofDigits b []
[PROOFSTEP]
change k ∣ 0 - 0
[GOAL]
case nil
n : ℕ
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ 0 - 0
[PROOFSTEP]
simp
[GOAL]
case cons
n : ℕ
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ ofDigits a (d :: L) - ofDigits b (d :: L)
[PROOFSTEP]
simp only [ofDigits, add_sub_add_left_eq_sub]
[GOAL]
case cons
n : ℕ
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ a * ofDigits a L - b * ofDigits b L
[PROOFSTEP]
exact dvd_mul_sub_mul h ih
[GOAL]
n b b' k : ℕ
h : b ≡ b' [MOD k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [MOD k]
[PROOFSTEP]
induction' L with d L ih
[GOAL]
case nil
n b b' k : ℕ
h : b ≡ b' [MOD k]
⊢ ofDigits b [] ≡ ofDigits b' [] [MOD k]
[PROOFSTEP]
rfl
[GOAL]
case cons
n b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [MOD k]
[PROOFSTEP]
dsimp [ofDigits]
[GOAL]
case cons
n b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ d + b * ofDigits b L ≡ d + b' * ofDigits b' L [MOD k]
[PROOFSTEP]
dsimp [Nat.ModEq] at *
[GOAL]
case cons
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d + b * ofDigits b L) % k = (d + b' * ofDigits b' L) % k
[PROOFSTEP]
conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]
[GOAL]
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b * ofDigits b L) % k
[PROOFSTEP]
rw [Nat.add_mod, Nat.mul_mod, h, ih]
[GOAL]
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b * ofDigits b L) % k
[PROOFSTEP]
rw [Nat.add_mod, Nat.mul_mod, h, ih]
[GOAL]
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b * ofDigits b L) % k
[PROOFSTEP]
rw [Nat.add_mod, Nat.mul_mod, h, ih]
[GOAL]
case cons
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
[PROOFSTEP]
conv_rhs => rw [Nat.add_mod, Nat.mul_mod]
[GOAL]
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b' * ofDigits b' L) % k
[PROOFSTEP]
rw [Nat.add_mod, Nat.mul_mod]
[GOAL]
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b' * ofDigits b' L) % k
[PROOFSTEP]
rw [Nat.add_mod, Nat.mul_mod]
[GOAL]
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b' * ofDigits b' L) % k
[PROOFSTEP]
rw [Nat.add_mod, Nat.mul_mod]
[GOAL]
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
[PROOFSTEP]
induction' L with d L ih
[GOAL]
case nil
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
⊢ ofDigits b [] ≡ ofDigits b' [] [ZMOD ↑k]
[PROOFSTEP]
rfl
[GOAL]
case cons
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [ZMOD ↑k]
[PROOFSTEP]
dsimp [ofDigits]
[GOAL]
case cons
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ↑d + b * ofDigits b L ≡ ↑d + b' * ofDigits b' L [ZMOD ↑k]
[PROOFSTEP]
dsimp [Int.ModEq] at *
[GOAL]
case cons
n : ℕ
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
⊢ (↑d + b * ofDigits b L) % ↑k = (↑d + b' * ofDigits b' L) % ↑k
[PROOFSTEP]
conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]
[GOAL]
n : ℕ
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d + b * ofDigits b L) % ↑k
[PROOFSTEP]
rw [Int.add_emod, Int.mul_emod, h, ih]
[GOAL]
n : ℕ
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d + b * ofDigits b L) % ↑k
[PROOFSTEP]
rw [Int.add_emod, Int.mul_emod, h, ih]
[GOAL]
n : ℕ
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d + b * ofDigits b L) % ↑k
[PROOFSTEP]
rw [Int.add_emod, Int.mul_emod, h, ih]
[GOAL]
case cons
n : ℕ
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
⊢ (↑d % ↑k + b' % ↑k * (ofDigits b' L % ↑k) % ↑k) % ↑k = (↑d + b' * ofDigits b' L) % ↑k
[PROOFSTEP]
conv_rhs => rw [Int.add_emod, Int.mul_emod]
[GOAL]
n : ℕ
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d + b' * ofDigits b' L) % ↑k
[PROOFSTEP]
rw [Int.add_emod, Int.mul_emod]
[GOAL]
n : ℕ
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d + b' * ofDigits b' L) % ↑k
[PROOFSTEP]
rw [Int.add_emod, Int.mul_emod]
[GOAL]
n : ℕ
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d + b' * ofDigits b' L) % ↑k
[PROOFSTEP]
rw [Int.add_emod, Int.mul_emod]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ List.sum (digits b' n) [MOD b]
[PROOFSTEP]
rw [← ofDigits_one]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ ofDigits 1 (digits b' n) [MOD b]
[PROOFSTEP]
conv =>
  congr
  ·skip
  ·rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| n ≡ ofDigits 1 (digits b' n) [MOD b]
[PROOFSTEP]
  congr
  ·skip
  ·rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| n ≡ ofDigits 1 (digits b' n) [MOD b]
[PROOFSTEP]
  congr
  ·skip
  ·rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| n ≡ ofDigits 1 (digits b' n) [MOD b]
[PROOFSTEP]
congr
[GOAL]
case n
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| b
case a
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| n
case b n✝ b b' : ℕ h : b' % b = 1 n : ℕ | ofDigits 1 (digits b' n)
[PROOFSTEP]
·skip
[GOAL]
case n
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| b
[PROOFSTEP]
skip
[GOAL]
case n
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| b
[PROOFSTEP]
skip
[GOAL]
case n
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| b
[PROOFSTEP]
skip
[GOAL]
case a
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| n
case b n✝ b b' : ℕ h : b' % b = 1 n : ℕ | ofDigits 1 (digits b' n)
[PROOFSTEP]
·rw [← ofDigits_digits b' n]
[GOAL]
case a
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| n
[PROOFSTEP]
rw [← ofDigits_digits b' n]
[GOAL]
case a
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| n
[PROOFSTEP]
rw [← ofDigits_digits b' n]
[GOAL]
case a
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| n
[PROOFSTEP]
rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (digits b' n) ≡ ofDigits 1 (digits b' n) [MOD b]
[PROOFSTEP]
convert ofDigits_modEq b' b (digits b' n)
[GOAL]
case h.e'_3.h.e'_3
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ 1 = b' % b
[PROOFSTEP]
exact h.symm
[GOAL]
n✝ n : ℕ
⊢ 10 % 3 = 1
[PROOFSTEP]
norm_num
[GOAL]
n✝ n : ℕ
⊢ 10 % 9 = 1
[PROOFSTEP]
norm_num
[GOAL]
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ↑n ≡ ofDigits c (digits b' n) [ZMOD ↑b]
[PROOFSTEP]
conv =>
  congr
  ·skip
  ·rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n ≡ ofDigits c (digits b' n) [ZMOD ↑b]
[PROOFSTEP]
  congr
  ·skip
  ·rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n ≡ ofDigits c (digits b' n) [ZMOD ↑b]
[PROOFSTEP]
  congr
  ·skip
  ·rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n ≡ ofDigits c (digits b' n) [ZMOD ↑b]
[PROOFSTEP]
congr
[GOAL]
case n
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑b
case a
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n
case b n✝ b b' : ℕ c : ℤ h : ↑b' ≡ c [ZMOD ↑b] n : ℕ | ofDigits c (digits b' n)
[PROOFSTEP]
·skip
[GOAL]
case n
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑b
[PROOFSTEP]
skip
[GOAL]
case n
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑b
[PROOFSTEP]
skip
[GOAL]
case n
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑b
[PROOFSTEP]
skip
[GOAL]
case a
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n
case b n✝ b b' : ℕ c : ℤ h : ↑b' ≡ c [ZMOD ↑b] n : ℕ | ofDigits c (digits b' n)
[PROOFSTEP]
·rw [← ofDigits_digits b' n]
[GOAL]
case a
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n
[PROOFSTEP]
rw [← ofDigits_digits b' n]
[GOAL]
case a
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n
[PROOFSTEP]
rw [← ofDigits_digits b' n]
[GOAL]
case a
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n
[PROOFSTEP]
rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ↑(ofDigits b' (digits b' n)) ≡ ofDigits c (digits b' n) [ZMOD ↑b]
[PROOFSTEP]
rw [coe_int_ofDigits]
[GOAL]
n✝ b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ofDigits (↑b') (digits b' n) ≡ ofDigits c (digits b' n) [ZMOD ↑b]
[PROOFSTEP]
apply ofDigits_zmodeq' _ _ _ h
[GOAL]
n✝ n : ℕ
⊢ ofDigits (-1) [n] = List.alternatingSum (List.map (fun n => ↑n) [n])
[PROOFSTEP]
simp [ofDigits, List.alternatingSum]
[GOAL]
n a b : ℕ
t : List ℕ
⊢ ofDigits (-1) (a :: b :: t) = List.alternatingSum (List.map (fun n => ↑n) (a :: b :: t))
[PROOFSTEP]
simp only [ofDigits, List.alternatingSum, List.map_cons, ofDigits_neg_one t]
[GOAL]
n a b : ℕ
t : List ℕ
⊢ ↑a + -1 * (↑b + -1 * List.alternatingSum (List.map (fun n => ↑n) t)) =
    ↑a + -↑b + List.alternatingSum (List.map (fun n => ↑n) t)
[PROOFSTEP]
ring
[GOAL]
n✝ n : ℕ
⊢ ↑n ≡ List.alternatingSum (List.map (fun n => ↑n) (digits 10 n)) [ZMOD 11]
[PROOFSTEP]
have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; norm_num) n
[GOAL]
n✝ n : ℕ
⊢ ↑10 ≡ -1 [ZMOD ↑11]
[PROOFSTEP]
unfold Int.ModEq
[GOAL]
n✝ n : ℕ
⊢ ↑10 % ↑11 = -1 % ↑11
[PROOFSTEP]
norm_num
[GOAL]
n✝ n : ℕ
t : ↑n ≡ ofDigits (-1) (digits 10 n) [ZMOD ↑11]
⊢ ↑n ≡ List.alternatingSum (List.map (fun n => ↑n) (digits 10 n)) [ZMOD 11]
[PROOFSTEP]
rwa [ofDigits_neg_one] at t
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ List.sum (digits b' n)
[PROOFSTEP]
rw [← ofDigits_one]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ ofDigits 1 (digits b' n)
[PROOFSTEP]
conv_lhs => rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| b ∣ n
[PROOFSTEP]
rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| b ∣ n
[PROOFSTEP]
rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
| b ∣ n
[PROOFSTEP]
rw [← ofDigits_digits b' n]
[GOAL]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ ofDigits b' (digits b' n) ↔ b ∣ ofDigits 1 (digits b' n)
[PROOFSTEP]
rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]
[GOAL]
n✝ n : ℕ
⊢ 10 % 3 = 1
[PROOFSTEP]
norm_num
[GOAL]
n✝ n : ℕ
⊢ 10 % 9 = 1
[PROOFSTEP]
norm_num
[GOAL]
n✝ b b' : ℕ
c : ℤ
h : ↑b ∣ ↑b' - c
n : ℕ
⊢ b ∣ n ↔ ↑b ∣ ofDigits c (digits b' n)
[PROOFSTEP]
rw [← Int.coe_nat_dvd]
[GOAL]
n✝ b b' : ℕ
c : ℤ
h : ↑b ∣ ↑b' - c
n : ℕ
⊢ ↑b ∣ ↑n ↔ ↑b ∣ ofDigits c (digits b' n)
[PROOFSTEP]
exact dvd_iff_dvd_of_dvd_sub (zmodeq_ofDigits_digits b b' c (Int.modEq_iff_dvd.2 h).symm _).symm.dvd
[GOAL]
n : ℕ
⊢ 11 ∣ n ↔ 11 ∣ List.alternatingSum (List.map (fun n => ↑n) (digits 10 n))
[PROOFSTEP]
have t := dvd_iff_dvd_ofDigits 11 10 (-1 : ℤ) (by norm_num) n
[GOAL]
n : ℕ
⊢ ↑11 ∣ ↑10 - -1
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ ofDigits (-1) (digits 10 n)
⊢ 11 ∣ n ↔ 11 ∣ List.alternatingSum (List.map (fun n => ↑n) (digits 10 n))
[PROOFSTEP]
rw [ofDigits_neg_one] at t
[GOAL]
n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ List.alternatingSum (List.map (fun n => ↑n) (digits 10 n))
⊢ 11 ∣ n ↔ 11 ∣ List.alternatingSum (List.map (fun n => ↑n) (digits 10 n))
[PROOFSTEP]
exact t
[GOAL]
n : ℕ
p : List.Palindrome (digits 10 n)
h : Even (List.length (digits 10 n))
⊢ 11 ∣ n
[PROOFSTEP]
let dig := (digits 10 n).map (Coe.coe : ℕ → ℤ)
[GOAL]
n : ℕ
p : List.Palindrome (digits 10 n)
h : Even (List.length (digits 10 n))
dig : List ℤ := List.map Coe.coe (digits 10 n)
⊢ 11 ∣ n
[PROOFSTEP]
replace h : Even dig.length := by rwa [List.length_map]
[GOAL]
n : ℕ
p : List.Palindrome (digits 10 n)
h : Even (List.length (digits 10 n))
dig : List ℤ := List.map Coe.coe (digits 10 n)
⊢ Even (List.length dig)
[PROOFSTEP]
rwa [List.length_map]
[GOAL]
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
⊢ 11 ∣ n
[PROOFSTEP]
refine' eleven_dvd_iff.2 ⟨0, (_ : dig.alternatingSum = 0)⟩
[GOAL]
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
⊢ List.alternatingSum dig = 0
[PROOFSTEP]
have := dig.alternatingSum_reverse
[GOAL]
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
this : List.alternatingSum (List.reverse dig) = (-1) ^ (List.length dig + 1) • List.alternatingSum dig
⊢ List.alternatingSum dig = 0
[PROOFSTEP]
rw [(p.map _).reverse_eq, _root_.pow_succ, h.neg_one_pow, mul_one, neg_one_zsmul] at this
[GOAL]
n : ℕ
p : List.Palindrome (digits 10 n)
dig : List ℤ := List.map Coe.coe (digits 10 n)
h : Even (List.length dig)
this : List.alternatingSum (List.map Coe.coe (digits 10 n)) = -List.alternatingSum dig
⊢ List.alternatingSum dig = 0
[PROOFSTEP]
exact eq_zero_of_neg_eq this.symm
[GOAL]
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l ∧ 1 < b ∧ 0 < m
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
[PROOFSTEP]
rcases h with ⟨h, b2, m0⟩
[GOAL]
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
[PROOFSTEP]
have b0 : 0 < b := by linarith
[GOAL]
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
⊢ 0 < b
[PROOFSTEP]
linarith
[GOAL]
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
[PROOFSTEP]
have n0 : 0 < n := by linarith [mul_pos b0 m0]
[GOAL]
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
⊢ 0 < n
[PROOFSTEP]
linarith [mul_pos b0 m0]
[GOAL]
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ digits b n = r :: l ∧ 1 < b ∧ 0 < n
[PROOFSTEP]
refine' ⟨_, b2, n0⟩
[GOAL]
case intro.intro
n✝ b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : digits b m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ digits b n = r :: l
[PROOFSTEP]
obtain ⟨rfl, rfl⟩ := (Nat.div_mod_unique b0).2 ⟨e, hr⟩
[GOAL]
case intro.intro.intro
n✝ b n : ℕ
l : List ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
h : digits b (n / b) = l
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ digits b n = n % b :: l
[PROOFSTEP]
subst h
[GOAL]
case intro.intro.intro
n✝ b n : ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ digits b n = n % b :: digits b (n / b)
[PROOFSTEP]
exact Nat.digits_def' b2 n0
[GOAL]
n✝ b n : ℕ
n0 : 0 < n
nb : n < b
⊢ digits b n = [n] ∧ 1 < b ∧ 0 < n
[PROOFSTEP]
have b2 : 1 < b := lt_iff_add_one_le.mpr (le_trans (add_le_add_right (lt_iff_add_one_le.mp n0) 1) nb)
[GOAL]
n✝ b n : ℕ
n0 : 0 < n
nb : n < b
b2 : 1 < b
⊢ digits b n = [n] ∧ 1 < b ∧ 0 < n
[PROOFSTEP]
refine' ⟨_, b2, n0⟩
[GOAL]
n✝ b n : ℕ
n0 : 0 < n
nb : n < b
b2 : 1 < b
⊢ digits b n = [n]
[PROOFSTEP]
rw [Nat.digits_def' b2 n0, Nat.mod_eq_of_lt nb, (Nat.div_eq_zero_iff ((zero_le n).trans_lt nb)).2 nb, Nat.digits_zero]