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])
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
⊢ (b + 2) ^ List.length l ≤ (b + 2) * ofDigits (b + 2) l
rw [← List.dropLast_append_getLast hl]
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)
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])
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]
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
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)
apply Nat.mul_le_mul_left
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
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
refine' le_trans _ (Nat.le_add_left _ _)
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
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
have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]
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
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
convert Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1
no goals
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
rw [Nat.mul_one]
no goals
n b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : List.getLast l hl ≠ 0
⊢ 0 < List.getLast l hl
rwa [pos_iff_ne_zero]