-- Mathlib/Data/Nat/Digits.lean
theorem getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
    (digits b m).getLast (digits_ne_nil_iff_ne_zero.mpr hm) ≠ 0

Proof state:
case zero.zero
hm : 0 ≠ 0
⊢ (digits 0 0).getLast ⋯ ≠ 0

Tactic:
cases hm rfl

Result:
no goals

Proof state:
case succ.zero.succ
m : ℕ
hm : m + 1 ≠ 0
⊢ 1 ≠ 0

Tactic:
exact Nat.one_ne_zero

Result:
no goals

Proof state:
case zero
m : ℕ
hm : m ≠ 0
⊢ (digits 0 m).getLast ⋯ ≠ 0

Tactic:
cases m

Result:
case zero.zero
hm : 0 ≠ 0
⊢ (digits 0 0).getLast ⋯ ≠ 0

case zero.succ
n✝ : ℕ
hm : n✝ + 1 ≠ 0
⊢ (digits 0 (n✝ + 1)).getLast ⋯ ≠ 0

Proof state:
b m : ℕ
hm : m ≠ 0
⊢ (b.digits m).getLast ⋯ ≠ 0

Tactic:
rcases b with (_ | _ | b)

Result:
case zero
m : ℕ
hm : m ≠ 0
⊢ (digits 0 m).getLast ⋯ ≠ 0

case succ.zero
m : ℕ
hm : m ≠ 0
⊢ ((0 + 1).digits m).getLast ⋯ ≠ 0

case succ.succ
m : ℕ
hm : m ≠ 0
b : ℕ
⊢ ((b + 1 + 1).digits m).getLast ⋯ ≠ 0

Proof state:
case succ.succ
m b : ℕ
⊢ ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0

Tactic:
induction m using Nat.strongRecOn with | ind n IH => ?_

Result:
case succ.succ.ind
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
⊢ ∀ (hm : n ≠ 0), ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Proof state:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
rw [digits_getLast n (le_add_left 2 b)]

Result:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ ((b + 2).digits (n / (b + 2))).getLast ?neg.q✝ ≠ 0

case neg.q
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ (b + 2).digits (n / (b + 2)) ≠ []

Proof state:
case succ.zero.zero
hm : 0 ≠ 0
⊢ ((0 + 1).digits 0).getLast ⋯ ≠ 0

Tactic:
cases hm rfl

Result:
no goals

Proof state:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ 0 < n / b.succ.succ

Tactic:
exact Nat.div_pos (le_of_not_lt hnb) (zero_lt_succ (succ b))

Result:
no goals

Proof state:
case succ.succ.ind
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
by_cases hnb : n < b + 2

Result:
case pos
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : n < b + 2
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Proof state:
case succ.succ
m : ℕ
hm : m ≠ 0
b : ℕ
⊢ ((b + 1 + 1).digits m).getLast ⋯ ≠ 0

Tactic:
revert hm

Result:
case succ.succ
m b : ℕ
⊢ ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0

Proof state:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ ((b + 2).digits (n / (b + 2))).getLast ?neg.q✝ ≠ 0

case neg.q
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ (b + 2).digits (n / (b + 2)) ≠ []

Tactic:
refine IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) ?_

Result:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ n / b.succ.succ ≠ 0

Proof state:
case succ.zero.succ
n✝ : ℕ
hm : n✝ + 1 ≠ 0
⊢ ((0 + 1).digits (n✝ + 1)).getLast ⋯ ≠ 0

Tactic:
rename ℕ => m

Result:
case succ.zero.succ
m : ℕ
hm : m + 1 ≠ 0
⊢ ((0 + 1).digits (m + 1)).getLast ⋯ ≠ 0

Proof state:
case pos
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : n < b + 2
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
simpa only [digits_of_lt (b + 2) n hn hnb]

Result:
no goals

Proof state:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ n / b.succ.succ ≠ 0

Tactic:
rw [← pos_iff_ne_zero]

Result:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ 0 < n / b.succ.succ

Proof state:
case succ.zero.succ
m : ℕ
hm : m + 1 ≠ 0
⊢ ((0 + 1).digits (m + 1)).getLast ⋯ ≠ 0

Tactic:
simp only [zero_add, digits_one, List.getLast_replicate_succ m 1]

Result:
case succ.zero.succ
m : ℕ
hm : m + 1 ≠ 0
⊢ 1 ≠ 0

Proof state:
case succ.succ.ind
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
⊢ ∀ (hm : n ≠ 0), ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
intro hn

Result:
case succ.succ.ind
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Proof state:
case zero.succ
n✝ : ℕ
hm : n✝ + 1 ≠ 0
⊢ (digits 0 (n✝ + 1)).getLast ⋯ ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.zero
m : ℕ
hm : m ≠ 0
⊢ ((0 + 1).digits m).getLast ⋯ ≠ 0

Tactic:
cases m

Result:
case succ.zero.zero
hm : 0 ≠ 0
⊢ ((0 + 1).digits 0).getLast ⋯ ≠ 0

case succ.zero.succ
n✝ : ℕ
hm : n✝ + 1 ≠ 0
⊢ ((0 + 1).digits (n✝ + 1)).getLast ⋯ ≠ 0