chore(data/nat/digits): refactor proof of last_digit_ne_zero (#3836)

I thoroughly misunderstood why my prior attempts for #3544 weren't working. I've refactored the proof so the `private` lemma is no longer necessary.

src/data/nat/digits.lean

@@ -273,33 +273,27 @@ lemma digits_last {b m : ℕ} (h : 2 ≤ b) (hm : 0 < m) (p q) :
   (digits b m).last p = (digits b (m/b)).last q :=
 by { simp only [digits_last_aux h hm], rw list.last_cons }
 
-private lemma last_digit_ne_zero_aux (b : ℕ) {m : ℕ} (hm : m ≠ 0) (p) :
-  (digits b m).last p ≠ 0 :=
+lemma last_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
+  (digits b m).last (digits_ne_nil_iff_ne_zero.mpr hm) ≠ 0 :=
 begin
   rcases b with _|_|b,
   { cases m; finish },
   { cases m, { finish },
     simp_rw [digits_one, list.last_repeat_succ 1 m],
     norm_num },
-  revert hm p,
+  revert hm,
   apply nat.strong_induction_on m,
-  intros n IH hn p,
+  intros n IH hn,
   have hnpos : 0 < n := nat.pos_of_ne_zero hn,
   by_cases hnb : n < b + 2,
   { simp_rw [digits_of_lt b.succ.succ n hnpos hnb],
     exact nat.pos_iff_ne_zero.mp hnpos },
   { rw digits_last (show 2 ≤ b + 2, from dec_trivial) hnpos,
-    refine IH _ (nat.div_lt_self hnpos dec_trivial) _ _,
+    refine IH _ (nat.div_lt_self hnpos dec_trivial) _,
     { rw ←nat.pos_iff_ne_zero,
-      exact nat.div_pos (le_of_not_lt hnb) dec_trivial },
-    { rw [digits_ne_nil_iff_ne_zero, ←nat.pos_iff_ne_zero],
       exact nat.div_pos (le_of_not_lt hnb) dec_trivial } },
 end
 
-lemma last_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
-  (digits b m).last (digits_ne_nil_iff_ne_zero.mpr hm) ≠ 0 :=
-last_digit_ne_zero_aux b hm $ digits_ne_nil_iff_ne_zero.mpr hm
-
 /-- The digits in the base b+2 expansion of n are all less than b+2 -/
 lemma digits_lt_base' {b m : ℕ} : ∀ {d}, d ∈ digits (b+2) m → d < b+2 :=
 begin