chore(data/nat/digits): golf, use seemingly weaker assumptions (#18203)

* Golf.
* Assume `n ≠ 0` instead of `0 < n` or `1 ≤ n`.
* Assume `1 < n` instead of `2 ≤ n`.
* Add `nat.exists_eq_add_of_le'` (forward-ported in leanprover-community/mathlib4#1662).

src/data/nat/basic.lean

@@ -210,18 +210,14 @@ by { rw ←not_iff_not, push_neg, exact forall_lt_succ }
 @[simp] theorem add_def {a b : ℕ} : nat.add a b = a + b := rfl
 @[simp] theorem mul_def {a b : ℕ} : nat.mul a b = a * b := rfl
 
-lemma exists_eq_add_of_le : ∀ {m n : ℕ}, m ≤ n → ∃ k : ℕ, n = m + k
-| 0 0 h := ⟨0, by simp⟩
-| 0 (n+1) h := ⟨n+1, by simp⟩
-| (m+1) (n+1) h :=
-  let ⟨k, hk⟩ := exists_eq_add_of_le (nat.le_of_succ_le_succ h) in
-  ⟨k, by simp [hk, add_comm, add_left_comm]⟩
-
-lemma exists_eq_add_of_lt : ∀ {m n : ℕ}, m < n → ∃ k : ℕ, n = m + k + 1
-| 0 0 h := false.elim $ lt_irrefl _ h
-| 0 (n+1) h := ⟨n, by simp⟩
-| (m+1) (n+1) h := let ⟨k, hk⟩ := exists_eq_add_of_le (nat.le_of_succ_le_succ h) in
-  ⟨k, by simp [hk]⟩
+lemma exists_eq_add_of_le (h : m ≤ n) : ∃ k : ℕ, n = m + k :=
+⟨n - m, (nat.add_sub_of_le h).symm⟩
+
+lemma exists_eq_add_of_le' (h : m ≤ n) : ∃ k : ℕ, n = k + m :=
+⟨n - m, (nat.sub_add_cancel h).symm⟩
+
+lemma exists_eq_add_of_lt (h : m < n) : ∃ k : ℕ, n = m + k + 1 :=
+⟨n - (m + 1), by rw [add_right_comm, nat.add_sub_of_le h]⟩
 
 /-! ### `pred` -/
 

src/data/nat/digits.lean

@@ -79,8 +79,8 @@ by rcases b with _|⟨_|⟨_⟩⟩; simp [digits, digits_aux_0, digits_aux_1]
 
 @[simp] lemma digits_zero_succ (n : ℕ) : digits 0 (n.succ) = [n+1] := rfl
 
-theorem digits_zero_succ' : ∀ {n : ℕ} (w : 0 < n), digits 0 n = [n]
-| 0 h := absurd h dec_trivial
+theorem digits_zero_succ' : ∀ {n : ℕ}, n ≠ 0 → digits 0 n = [n]
+| 0 h := (h rfl).elim
 | (n+1) _ := rfl
 
 @[simp] lemma digits_one (n : ℕ) : digits 1 n = list.replicate n 1 := rfl
@@ -91,40 +91,31 @@ theorem digits_zero_succ' : ∀ {n : ℕ} (w : 0 < n), digits 0 n = [n]
   digits (b+2) (n+1) = (((n+1) % (b+2)) :: digits (b+2) ((n+1) / (b+2))) :=
 by { rw [digits, digits_aux_def], exact succ_pos n }
 
-theorem digits_def' : ∀ {b : ℕ} (h : 2 ≤ b) {n : ℕ} (w : 0 < n),
+theorem digits_def' : ∀ {b : ℕ} (h : 1 < b) {n : ℕ} (w : 0 < n),
   digits b n = n % b :: digits b (n/b)
 | 0 h := absurd h dec_trivial
 | 1 h := absurd h dec_trivial
 | (b+2) h := digits_aux_def _ _
 
-@[simp]
-lemma digits_of_lt (b x : ℕ) (w₁ : 0 < x) (w₂ : x < b) : digits b x = [x] :=
+@[simp] lemma digits_of_lt (b x : ℕ) (hx : x ≠ 0) (hxb : x < b) : digits b x = [x] :=
 begin
-  cases b,
-  { cases w₂ },
-  { cases b,
-    { interval_cases x, },
-    { cases x,
-      { cases w₁, },
-      { rw [digits_add_two_add_one, nat.div_eq_of_lt w₂, digits_zero, nat.mod_eq_of_lt w₂] } } }
+  rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩,
+  rcases exists_eq_add_of_le' ((nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩,
+  rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]
 end
 
-lemma digits_add (b : ℕ) (h : 2 ≤ b) (x y : ℕ) (w : x < b) (w' : 0 < x ∨ 0 < y) :
+lemma digits_add (b : ℕ) (h : 1 < b) (x y : ℕ) (hxb : x < b) (hxy : x ≠ 0 ∨ y ≠ 0) :
   digits b (x + b * y) = x :: digits b y :=
 begin
-  cases b,
-  { cases h, },
-  { cases b,
-    { norm_num at h, },
-    { cases y,
-      { norm_num at w',
-        simp [w, w'], },
-      dsimp [digits],
-      rw digits_aux_def,
-      { congr,
-        { simp [nat.add_mod, nat.mod_eq_of_lt w], },
-        { simp [mul_comm (b+2), nat.add_mul_div_right, nat.div_eq_of_lt w], } },
-      { apply nat.succ_pos, }, }, },
+  rcases exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩,
+  cases y,
+  { simp [hxb, hxy.resolve_right (absurd rfl)] },
+  dsimp [digits],
+  rw digits_aux_def,
+  { congr,
+    { simp [nat.add_mod, mod_eq_of_lt hxb], },
+    { simp [add_mul_div_left, div_eq_of_lt hxb] } },
+  { apply nat.succ_pos }
 end
 
 /--
@@ -201,22 +192,14 @@ begin
   { dsimp [of_digits], push_cast }
 end
 
-lemma digits_zero_of_eq_zero {b : ℕ} (h : 1 ≤ b) {L : list ℕ} (w : of_digits b L = 0) :
-  ∀ l ∈ L, l = 0 :=
-begin
-  induction L with d L ih,
-  { intros l m,
-    cases m, },
-  { intros l m,
-    dsimp [of_digits] at w,
-    rcases m with ⟨rfl⟩,
-    { apply nat.eq_zero_of_add_eq_zero_right w },
-    { exact ih (mul_right_injective₀ (pos_iff_ne_zero.1 h)
-        (nat.eq_zero_of_add_eq_zero_left w)) _ m, }, }
-end
+lemma digits_zero_of_eq_zero {b : ℕ} (h : b ≠ 0) :
+  ∀ {L : list ℕ} (h0 : of_digits b L = 0) (l ∈ L), l = 0
+| (a :: L) h0 l (or.inl rfl) := nat.eq_zero_of_add_eq_zero_right h0
+| (a :: L) h0 l (or.inr hL) :=
+  digits_zero_of_eq_zero (mul_right_injective₀ h (nat.eq_zero_of_add_eq_zero_left h0)) _ hL
 
 lemma digits_of_digits
-  (b : ℕ) (h : 2 ≤ b) (L : list ℕ)
+  (b : ℕ) (h : 1 < b) (L : list ℕ)
   (w₁ : ∀ l ∈ L, l < b) (w₂ : ∀ (h : L ≠ []), L.last h ≠ 0) :
   digits b (of_digits b L) = L :=
 begin
@@ -233,17 +216,13 @@ begin
     { exact w₁ d (list.mem_cons_self _ _) },
     { by_cases h' : L = [],
       { rcases h' with rfl,
-        simp at w₂,
         left,
-        apply nat.pos_of_ne_zero,
-        exact w₂ },
+        simpa using w₂ },
       { right,
-        apply nat.pos_of_ne_zero,
         contrapose! w₂,
-        apply digits_zero_of_eq_zero _ w₂,
-        { rw list.last_cons h',
-          exact list.last_mem h', },
-        { exact le_of_lt h, }, }, }, },
+        refine digits_zero_of_eq_zero h.ne_bot w₂ _ _,
+        rw list.last_cons h',
+        exact list.last_mem h' } } }
 end
 
 lemma of_digits_digits (b n : ℕ) : of_digits b (digits b n) = n :=
@@ -295,7 +274,7 @@ end
 lemma digits_ne_nil_iff_ne_zero {b n : ℕ} : digits b n ≠ [] ↔ n ≠ 0 :=
 not_congr digits_eq_nil_iff_eq_zero
 
-lemma digits_eq_cons_digits_div {b n : ℕ} (h : 2 ≤ b) (w : 0 < n) :
+lemma digits_eq_cons_digits_div {b n : ℕ} (h : 1 < b) (w : n ≠ 0) :
   digits b n = ((n % b) :: digits b (n / b)) :=
 begin
   rcases b with _|_|b,
@@ -306,12 +285,12 @@ begin
   simp,
 end
 
-lemma digits_last {b : ℕ} (m : ℕ) (h : 2 ≤ b) (p q) :
+lemma digits_last {b : ℕ} (m : ℕ) (h : 1 < b) (p q) :
   (digits b m).last p = (digits b (m/b)).last q :=
 begin
   by_cases hm : m = 0,
   { simp [hm], },
-  simp only [digits_eq_cons_digits_div h (nat.pos_of_ne_zero hm)],
+  simp only [digits_eq_cons_digits_div h hm],
   rw list.last_cons,
 end
 
@@ -322,21 +301,20 @@ function.left_inverse.injective (of_digits_digits b)
   b.digits n = b.digits m ↔ n = m :=
 (digits.injective b).eq_iff
 
-lemma digits_len (b n : ℕ) (hb : 2 ≤ b) (hn : 0 < n) :
+lemma digits_len (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) :
   (b.digits n).length = b.log n + 1 :=
 begin
   induction n using nat.strong_induction_on with n IH,
   rw [digits_eq_cons_digits_div hb hn, list.length],
-  cases (n / b).eq_zero_or_pos with h h,
-  { have posb : 0 < b := zero_lt_two.trans_le hb,
-    simp [h, log_eq_zero_iff, ←nat.div_eq_zero_iff posb] },
+  by_cases h : n / b = 0,
+  { have hb0 : b ≠ 0 := (nat.succ_le_iff.1 hb).ne_bot,
+    simp [h, log_eq_zero_iff, ← nat.div_eq_zero_iff hb0.bot_lt] },
   { have hb' : 1 < b := one_lt_two.trans_le hb,
-    have : n / b < n := div_lt_self hn hb',
+    have : n / b < n := div_lt_self (nat.pos_of_ne_zero hn) hb',
     rw [IH _ this h, log_div_base, tsub_add_cancel_of_le],
-    rw [succ_le_iff],
-    refine log_pos hb' _,
+    refine nat.succ_le_of_lt (log_pos hb' _),
     contrapose! h,
-    rw div_eq_of_lt h }
+    exact div_eq_of_lt h }
 end
 
 lemma last_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
@@ -351,12 +329,10 @@ begin
   revert hm,
   apply nat.strong_induction_on m,
   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 pos_iff_ne_zero.mp hnpos },
+  { simpa only [digits_of_lt (b + 2) n hn hnb] },
   { rw digits_last n (show 2 ≤ b + 2, from dec_trivial),
-    refine IH _ (nat.div_lt_self hnpos dec_trivial) _,
+    refine IH _ (nat.div_lt_self hn.bot_lt dec_trivial) _,
     { rw ←pos_iff_ne_zero,
       exact nat.div_pos (le_of_not_lt hnb) dec_trivial } },
 end
@@ -375,7 +351,7 @@ begin
 end
 
 /-- The digits in the base b expansion of n are all less than b, if b ≥ 2 -/
-lemma digits_lt_base {b m d : ℕ} (hb : 2 ≤ b) (hd : d ∈ digits b m) : d < b :=
+lemma digits_lt_base {b m d : ℕ} (hb : 1 < b) (hd : d ∈ digits b m) : d < b :=
 begin
   rcases b with _ | _ | b; try {linarith},
   exact digits_lt_base' hd,
@@ -397,8 +373,8 @@ begin
     exact hl hd (list.mem_cons_self _ _) }
 end
 
-/-- an n-digit number in base b is less than b^n if b ≥ 2 -/
-lemma of_digits_lt_base_pow_length {b : ℕ} {l : list ℕ} (hb : 2 ≤ b) (hl : ∀ x ∈ l, x < b) :
+/-- an n-digit number in base b is less than b^n if b > 1 -/
+lemma of_digits_lt_base_pow_length {b : ℕ} {l : list ℕ} (hb : 1 < b) (hl : ∀ x ∈ l, x < b) :
   of_digits b l < b^l.length :=
 begin
   rcases b with _ | _ | b; try { linarith },
@@ -413,7 +389,7 @@ begin
 end
 
 /-- Any number m is less than b^(number of digits in the base b representation of m) -/
-lemma lt_base_pow_length_digits {b m : ℕ} (hb : 2 ≤ b) : m < b^(digits b m).length :=
+lemma lt_base_pow_length_digits {b m : ℕ} (hb : 1 < b) : m < b^(digits b m).length :=
 begin
   rcases b with _ | _ | b; try { linarith },
   exact lt_base_pow_length_digits',
@@ -425,13 +401,10 @@ by rw [of_digits_append, of_digits_digits, of_digits_digits]
 
 lemma digits_len_le_digits_len_succ (b n : ℕ) : (digits b n).length ≤ (digits b (n + 1)).length :=
 begin
-  rcases n.eq_zero_or_pos with rfl|hn,
+  rcases decidable.eq_or_ne n 0 with rfl|hn,
   { simp },
-  cases lt_or_le b 2 with hb hb,
-  { rcases b with _|_|b,
-    { simp [digits_zero_succ', hn] },
-    { simp, },
-    { simpa [succ_lt_succ_iff] using hb } },
+  cases le_or_lt b 1 with hb hb,
+  { interval_cases b; simp [digits_zero_succ', hn] },
   simpa [digits_len, hb, hn] using log_mono_right (le_succ _)
 end
 
@@ -466,7 +439,7 @@ end
 Any non-zero natural number `m` is greater than
 b^((number of digits in the base b representation of m) - 1)
 -/
-lemma base_pow_length_digits_le (b m : ℕ) (hb : 2 ≤ b): m ≠ 0 → b ^ ((digits b m).length) ≤ b * m :=
+lemma base_pow_length_digits_le (b m : ℕ) (hb : 1 < b): m ≠ 0 → b ^ ((digits b m).length) ≤ b * m :=
 begin
   rcases b with _ | _ | b; try { linarith },
   exact base_pow_length_digits_le' b m,
@@ -480,11 +453,10 @@ begin
   { simp, },
   rw bits_append_bit _ _ (λ hn, absurd hn h),
   cases b,
-  { rw digits_def' (le_refl 2),
+  { rw digits_def' one_lt_two,
      { simpa [nat.bit, nat.bit0_val n], },
      { simpa [pos_iff_ne_zero, bit_eq_zero_iff], }, },
-  { simpa [nat.bit, nat.bit1_val n, add_comm, digits_add 2 le_rfl 1 n (by norm_num)
-    (by norm_num)] },
+  { simpa [nat.bit, nat.bit1_val n, add_comm, digits_add 2 one_lt_two 1 n] },
 end
 
 
@@ -629,8 +601,8 @@ theorem digits_succ
   (b n m r l)
   (e : r + b * m = n)
   (hr : r < b)
-  (h : nat.digits b m = l ∧ 2 ≤ b ∧ 0 < m) :
-  nat.digits b n = r :: l ∧ 2 ≤ b ∧ 0 < n :=
+  (h : nat.digits b m = l ∧ 1 < b ∧ 0 < m) :
+  nat.digits b n = r :: l ∧ 1 < b ∧ 0 < n :=
 begin
   rcases h with ⟨h, b2, m0⟩,
   have b0 : 0 < b := by linarith,
@@ -642,12 +614,12 @@ end
 
 theorem digits_one
   (b n) (n0 : 0 < n) (nb : n < b) :
-  nat.digits b n = [n] ∧ 2 ≤ b ∧ 0 < n :=
+  nat.digits b n = [n] ∧ 1 < b ∧ 0 < n :=
 begin
-  have b2 : 2 ≤ b := by linarith,
+  have b2 : 1 < b := by linarith,
   refine ⟨_, b2, n0⟩,
   rw [nat.digits_def' b2 n0, nat.mod_eq_of_lt nb,
-    (nat.div_eq_zero_iff (by linarith : 0 < b)).2 nb, nat.digits_zero],
+    (nat.div_eq_zero_iff ((zero_le n).trans_lt nb)).2 nb, nat.digits_zero],
 end
 
 open tactic
@@ -685,11 +657,10 @@ example : nat.digits 10 123 = [3,2,1] := by norm_num
   if n = 0 then return (`([] : list ℕ), `(nat.digits_zero %%eb))
   else if b = 0 then do
     ic ← mk_instance_cache `(ℕ),
-    (_, pn0) ← norm_num.prove_pos ic en,
+    (_, pn0) ← norm_num.prove_ne_zero' ic en,
     return (`([%%en] : list ℕ), `(@nat.digits_zero_succ' %%en %%pn0))
   else if b = 1 then do
     ic ← mk_instance_cache `(ℕ),
-    (_, pn0) ← norm_num.prove_pos ic en,
     s ← simp_lemmas.add_simp simp_lemmas.mk `list.replicate,
     (rhs, p2, _) ← simplify s [] `(list.replicate %%en 1),
     p ← mk_eq_trans `(nat.digits_one %%en) p2,