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 []

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)
n b : ℕ
l : List ℕ
hl : ∀ (x : ℕ), x ∈ l → x < b + 2
⊢ ofDigits (b + 2) l < (b + 2) ^ List.length l
induction' l with hd tl IH
no goals
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 []
simp [ofDigits]
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)
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)
rw [ofDigits, List.length_cons, pow_succ]
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)
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)
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 _)
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
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)
suffices ↑hd < b + 2 by linarith
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
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
norm_cast
no goals
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
exact hl hd (List.mem_cons_self _ _)
no goals
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
rfl
no goals
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
simp only [zero_le]
no goals
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)
linarith