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
n b : ℕ
l : List ℕ
hb : 1 < b
hl : ∀ (x : ℕ), x ∈ l → x < b
⊢ ofDigits b l < b ^ List.length l
rcases b with (_ | _ | b) <;> try simp_all
no goals
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
exact ofDigits_lt_base_pow_length' hl
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
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
simp_all