[Merged by Bors] - feat(data/nat/digits): add last_digit_ne_zero

[shingtaklam1324]

The proof of base_pow_length_digits_le was refactored as suggested by @fpvandoorn in #3498.

---

[fpvandoorn]

The proof of the final result looks much better now! Thanks for making these changes.

[fpvandoorn]

This lemma would be more convenient if you remove the argument p and explicitly prove it using digits_ne_nil_iff_ne_zero.mpr hm.

[shingtaklam1324]

To be honest that was my first approach to use digits_ne_nil_iff_ne_zero.mpr hm. I really struggled to get nat.strong_induction_on to work with it, hence I've generalized over the proof. (see the use of revert p in the proof). There might be a better approach but this is the best I could come up with.

I can mark this as private and add in a lemma with the proof provided, would that be ok? So change this to private lemma last_digit_ne_zero_aux and add

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 m hm (digits_ne_nil_iff_ne_zero.mpr hm)

[shingtaklam1324]

I've done the above. So marked this one as private lemma last_digit_ne_zero_aux and then added another lemma that fills in the proof.

[fpvandoorn]

That works. Another option was to use as first tactic generalize : digits_ne_nil_iff_ne_zero.mpr hm = p,

[shingtaklam1324]

For this, I think m can be figured out by later hypotheses, but b can't be. Right?

Although in the only use of this lemma so far, b could be inferred.

[fpvandoorn]

That is correct. It depends a bit on the lemma whether we make the argument b explicit in this case (most of the time, but not always, b can be figured out from the statement you're proving at that time).

[fpvandoorn]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Run tests and docs
• Lint mathlib
• Build mathlib