refactor(data/nat/log): Golf + improved theorem names (#14019)

Other than golfing and moving a few things around, our main changes are:
- rename `log_le_log_of_le` to `log_mono_right`, analogous renames elsewhere.
- add `lt_pow_iff_log_lt` and a `clog` analog.

src/data/nat/choose/central.lean

@@ -132,7 +132,7 @@ lemma padic_val_nat_central_binom_of_large_le_one (hp : p.prime) (p_large : 2 *
   (padic_val_nat p (central_binom n)) ≤ 1 :=
 begin
   have log_weak_bound : log p (2 * n) ≤ 2,
-  { calc log p (2 * n) ≤ log p (p ^ 2) : log_le_log_of_le (le_of_lt p_large)
+  { calc log p (2 * n) ≤ log p (p ^ 2) : log_mono_right (le_of_lt p_large)
     ... = 2 : log_pow hp.one_lt 2, },
 
   have log_bound : log p (2 * n) ≤ 1,
@@ -146,7 +146,7 @@ begin
         { rw pow_two,
           exact (nat.le_div_iff_mul_le _ _ (prime.pos hp)).1 v.2.2, },
         exact lt_irrefl _ (lt_of_le_of_lt bad p_large), },
-      { rw log_eq_zero (or.inl h),
+      { rw log_of_lt h,
         exact zero_le 1, }, }, },
 
   exact le_trans (padic_val_nat_central_binom_le hp) log_bound,

src/data/nat/digits.lean

@@ -432,7 +432,7 @@ begin
     { simp [digits_zero_succ', hn] },
     { simp, },
     { simpa [succ_lt_succ_iff] using hb } },
-  simpa [digits_len, hb, hn] using log_le_log_of_le (le_succ _)
+  simpa [digits_len, hb, hn] using log_mono_right (le_succ _)
 end
 
 lemma le_digits_len_le (b n m : ℕ) (h : n ≤ m) : (digits b n).length ≤ (digits b m).length :=

src/data/nat/log.lean

@@ -31,32 +31,28 @@ such that `b^k ≤ n`, so if `b^k = n`, it returns exactly `k`. -/
     log (n / b) + 1
   else 0
 
-lemma log_eq_zero {b n : ℕ} (hnb : n < b ∨ b ≤ 1) : log b n = 0 :=
+private lemma log_eq_zero_aux {b n : ℕ} (hnb : n < b ∨ b ≤ 1) : log b n = 0 :=
 begin
   rw [or_iff_not_and_not, not_lt, not_le] at hnb,
-  rw [log, ←ite_not, if_pos hnb],
+  rw [log, ←ite_not, if_pos hnb]
 end
 
-lemma log_of_one_lt_of_le {b n : ℕ} (h : 1 < b) (hn : b ≤ n) : log b n = log b (n / b) + 1 :=
-begin
-  rw log,
-  exact if_pos ⟨hn, h⟩,
-end
+lemma log_of_lt {b n : ℕ} (hb : n < b) : log b n = 0 :=
+log_eq_zero_aux (or.inl hb)
 
-lemma log_of_lt {b n : ℕ} (hnb : n < b) : log b n = 0 :=
-by rw [log, if_neg (λ h : b ≤ n ∧ 1 < b, h.1.not_lt hnb)]
+lemma log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n) : log b n = 0 :=
+log_eq_zero_aux (or.inr hb)
 
-lemma log_of_left_le_one {b n : ℕ} (hb : b ≤ 1) : log b n = 0 :=
-by rw [log, if_neg (λ h : b ≤ n ∧ 1 < b, h.2.not_le hb)]
+lemma log_of_one_lt_of_le {b n : ℕ} (h : 1 < b) (hn : b ≤ n) : log b n = log b (n / b) + 1 :=
+by { rw log, exact if_pos ⟨hn, h⟩ }
 
 lemma log_eq_zero_iff {b n : ℕ} : log b n = 0 ↔ n < b ∨ b ≤ 1 :=
-begin
-  refine ⟨λ h_log, _, log_eq_zero⟩,
+⟨λ h_log, begin
   by_contra' h,
   have := log_of_one_lt_of_le h.2 h.1,
   rw h_log at this,
   exact succ_ne_zero _ this.symm
-end
+end, log_eq_zero_aux⟩
 
 lemma log_eq_one_iff {b n : ℕ} : log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n :=
 -- This is best possible: if b = 2, n = 5, then 1 < b and b ≤ n but n > b * b.
@@ -78,24 +74,23 @@ begin
     exact or.inl h, },
 end
 
-@[simp] lemma log_zero_left (n : ℕ) : log 0 n = 0 :=
+@[simp] lemma log_zero_left : ∀ n, log 0 n = 0 :=
 log_of_left_le_one zero_le_one
 
 @[simp] lemma log_zero_right (b : ℕ) : log b 0 = 0 :=
 by { rw log, cases b; refl }
 
-@[simp] lemma log_one_left (n : ℕ) : log 1 n = 0 :=
+@[simp] lemma log_one_left : ∀ n, log 1 n = 0 :=
 log_of_left_le_one le_rfl
 
 @[simp] lemma log_one_right (b : ℕ) : log b 1 = 0 :=
 if h : b ≤ 1 then
-  log_of_left_le_one h
+  log_of_left_le_one h 1
 else
   log_of_lt (not_le.mp h)
 
 /-- `pow b` and `log b` (almost) form a Galois connection. -/
-lemma pow_le_iff_le_log {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : 0 < y) :
-  b^x ≤ y ↔ x ≤ log b y :=
+lemma pow_le_iff_le_log {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : 0 < y) : b ^ x ≤ y ↔ x ≤ log b y :=
 begin
   induction y using nat.strong_induction_on with y ih generalizing x,
   cases x,
@@ -109,6 +104,9 @@ begin
     exact (pow_one b).symm }
 end
 
+lemma lt_pow_iff_log_lt {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : 0 < y) : y < b ^ x ↔ log b y < x :=
+lt_iff_lt_of_le_iff_le (pow_le_iff_le_log hb hy)
+
 lemma log_pow {b : ℕ} (hb : 1 < b) (x : ℕ) : log b (b ^ x) = x :=
 eq_of_forall_le_iff $ λ z,
 by { rw ←pow_le_iff_le_log hb (pow_pos (zero_lt_one.trans hb) _),
@@ -141,7 +139,7 @@ end
 lemma pow_log_le_self {b : ℕ} (hb : 1 < b) {x : ℕ} (hx : 0 < x) : b ^ log b x ≤ x :=
 (pow_le_iff_le_log hb hx).2 le_rfl
 
-lemma log_le_log_of_le {b n m : ℕ} (h : n ≤ m) : log b n ≤ log b m :=
+@[mono] lemma log_mono_right {b n m : ℕ} (h : n ≤ m) : log b n ≤ log b m :=
 begin
   cases le_or_lt b 1 with hb hb,
   { rw log_of_left_le_one hb, exact zero_le _ },
@@ -151,63 +149,55 @@ begin
       exact (pow_log_le_self hb hn).trans h } }
 end
 
-lemma log_le_log_of_left_ge {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n ≤ log c n :=
+@[mono] lemma log_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n ≤ log c n :=
 begin
-  cases n, { simp },
-  rw ← pow_le_iff_le_log hc (zero_lt_succ n),
-  calc
-    c ^ log b n.succ ≤ b ^ log b n.succ : pow_le_pow_of_le_left
-                                            (le_of_lt $ zero_lt_one.trans hc) hb _
-                 ... ≤ n.succ           : pow_log_le_self (lt_of_lt_of_le hc hb)
-                                            (zero_lt_succ n)
+  cases n, { rw [log_zero_right, log_zero_right] },
+  rw ←pow_le_iff_le_log hc (zero_lt_succ n),
+  calc c ^ log b n.succ ≤ b ^ log b n.succ : pow_le_pow_of_le_left
+                                              (zero_lt_one.trans hc).le hb _
+                    ... ≤ n.succ           : pow_log_le_self (hc.trans_le hb)
+                                              (zero_lt_succ n)
 end
 
-lemma log_monotone {b : ℕ} : monotone (λ n : ℕ, log b n) :=
-λ x y, log_le_log_of_le
+lemma log_monotone {b : ℕ} : monotone (log b) :=
+λ x y, log_mono_right
 
 lemma log_antitone_left {n : ℕ} : antitone_on (λ b, log b n) (set.Ioi 1) :=
-λ _ hc _ _ hb, log_le_log_of_left_ge (set.mem_Iio.1 hc) hb
+λ _ hc _ _ hb, log_anti_left (set.mem_Iio.1 hc) hb
 
 @[simp] lemma log_div_mul_self (b n : ℕ) : log b (n / b * b) = log b n :=
-begin
-  refine eq_of_forall_le_iff (λ z, _),
-  split,
-  { intro h,
-    exact h.trans (log_monotone (div_mul_le_self _ _)) },
-  { intro h,
-    rcases b with _|_|b,
-    { simpa using h },
-    { simpa using h },
-    rcases n.zero_le.eq_or_lt with rfl|hn,
-    { simpa using h },
-    cases le_or_lt b.succ.succ n with hb hb,
-    { cases z,
-      { simp },
-      have : 0 < b.succ.succ := nat.succ_pos',
-      rw [←pow_le_iff_le_log, pow_succ'] at h ⊢,
-      { rwa [(strict_mono_mul_right_of_pos this).le_iff_le,
-             nat.le_div_iff_mul_le _ _ nat.succ_pos'] },
-      all_goals { simp [hn, nat.div_pos hb nat.succ_pos'] } },
-    { simpa [div_eq_of_lt, hb, log_eq_zero] using h } }
-end
+eq_of_forall_le_iff (λ z, ⟨λ h, h.trans (log_monotone (div_mul_le_self _ _)), λ h, begin
+  rcases b with _|_|b,
+  { rwa log_zero_left at * },
+  { rwa log_one_left at * },
+  rcases n.zero_le.eq_or_lt with rfl|hn,
+  { rwa [nat.zero_div, zero_mul] },
+  cases le_or_lt b.succ.succ n with hb hb,
+  { cases z,
+    { apply zero_le },
+    rw [←pow_le_iff_le_log, pow_succ'] at h ⊢,
+    { rwa [(strict_mono_mul_right_of_pos nat.succ_pos').le_iff_le,
+            nat.le_div_iff_mul_le _ _ nat.succ_pos'] },
+    all_goals { simp [hn, nat.div_pos hb nat.succ_pos'] } },
+  { simpa [div_eq_of_lt, hb, log_of_lt] using h }
+end⟩)
 
 @[simp] lemma log_div_base (b n : ℕ) : log b (n / b) = log b n - 1 :=
 begin
   cases lt_or_le n b with h h,
-  { simp [div_eq_of_lt, h, log_eq_zero] },
+  { rw [div_eq_of_lt h, log_of_lt h, log_zero_right] },
   rcases n.zero_le.eq_or_lt with rfl|hn,
-  { simp },
+  { rw [nat.zero_div, log_zero_right] },
   rcases b with _|_|b,
-  { simp },
-  { simp },
+  { rw [log_zero_left, log_zero_left] },
+  { rw [log_one_left, log_one_left] },
   rw [←succ_inj', ←succ_inj'],
   simp_rw succ_eq_add_one,
   rw [nat.sub_add_cancel, ←log_mul_base];
   { simp [succ_le_iff, log_pos, h, nat.div_pos] },
 end
 
-
-private lemma add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1)/b < n :=
+private lemma add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1) / b < n :=
 begin
   rw [div_lt_iff_lt_mul _ _ (zero_lt_one.trans hb), ←succ_le_iff, ←pred_eq_sub_one,
     succ_pred_eq_of_pos (add_pos (zero_lt_one.trans hn) (zero_lt_one.trans hb))],
@@ -260,8 +250,7 @@ begin
 end
 
 /--`clog b` and `pow b` form a Galois connection. -/
-lemma le_pow_iff_clog_le {b : ℕ} (hb : 1 < b) {x y : ℕ} :
-  x ≤ b^y ↔ clog b x ≤ y :=
+lemma le_pow_iff_clog_le {b : ℕ} (hb : 1 < b) {x y : ℕ} : x ≤ b ^ y ↔ clog b x ≤ y :=
 begin
   induction x using nat.strong_induction_on with x ih generalizing y,
   cases y,
@@ -279,6 +268,9 @@ begin
     (zero_le _) }
 end
 
+lemma pow_lt_iff_lt_clog {b : ℕ} (hb : 1 < b) {x y : ℕ} : b ^ y < x ↔ y < clog b x :=
+lt_iff_lt_of_le_iff_le (le_pow_iff_clog_le hb)
+
 lemma clog_pow (b x : ℕ) (hb : 1 < b) : clog b (b ^ x) = x :=
 eq_of_forall_ge_iff $ λ z,
 by { rw ←le_pow_iff_clog_le hb, exact (pow_right_strict_mono hb).le_iff_le }
@@ -293,27 +285,27 @@ end
 lemma le_pow_clog {b : ℕ} (hb : 1 < b) (x : ℕ) : x ≤ b ^ clog b x :=
 (le_pow_iff_clog_le hb).2 le_rfl
 
-lemma clog_le_clog_of_le (b : ℕ) {n m : ℕ} (h : n ≤ m) : clog b n ≤ clog b m :=
+@[mono] lemma clog_mono_right (b : ℕ) {n m : ℕ} (h : n ≤ m) : clog b n ≤ clog b m :=
 begin
   cases le_or_lt b 1 with hb hb,
   { rw clog_of_left_le_one hb, exact zero_le _ },
   { rw ←le_pow_iff_clog_le hb,
     exact h.trans (le_pow_clog hb _) }
 end
 
-lemma clog_le_clog_of_left_ge {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : clog b n ≤ clog c n :=
+@[mono] lemma clog_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : clog b n ≤ clog c n :=
 begin
   rw ← le_pow_iff_clog_le (lt_of_lt_of_le hc hb),
   calc
     n ≤ c ^ clog c n : le_pow_clog hc _
-  ... ≤ b ^ clog c n : pow_le_pow_of_le_left (le_of_lt $ zero_lt_one.trans hc) hb _
+  ... ≤ b ^ clog c n : pow_le_pow_of_le_left (zero_lt_one.trans hc).le hb _
 end
 
 lemma clog_monotone (b : ℕ) : monotone (clog b) :=
-λ x y, clog_le_clog_of_le _
+λ x y, clog_mono_right _
 
 lemma clog_antitone_left {n : ℕ} : antitone_on (λ b : ℕ, clog b n) (set.Ioi 1) :=
-λ _ hc _ _ hb, clog_le_clog_of_left_ge (set.mem_Iio.1 hc) hb
+λ _ hc _ _ hb, clog_anti_left (set.mem_Iio.1 hc) hb
 
 lemma log_le_clog (b n : ℕ) : log b n ≤ clog b n :=
 begin

src/data/nat/multiplicity.lean

@@ -97,7 +97,7 @@ lemma multiplicity_factorial {p : ℕ} (hp : p.prime) :
   calc multiplicity p (n+1)! = multiplicity p n! + multiplicity p (n+1) :
     by rw [factorial_succ, hp.multiplicity_mul, add_comm]
   ... = (∑ i in Ico 1 b, n / p ^ i : ℕ) + ((finset.Ico 1 b).filter (λ i, p ^ i ∣ n+1)).card :
-    by rw [multiplicity_factorial ((log_le_log_of_le $ le_succ _).trans_lt hb),
+    by rw [multiplicity_factorial ((log_mono_right $ le_succ _).trans_lt hb),
       ← multiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]
   ... = (∑ i in Ico 1 b, (n / p ^ i + if p^i ∣ n+1 then 1 else 0) : ℕ) :
     by { rw [sum_add_distrib, sum_boole], simp }
@@ -178,8 +178,8 @@ have h₁ : multiplicity p (choose n k) + multiplicity p (k! * (n - k)!) =
   begin
     rw [← hp.multiplicity_mul, ← mul_assoc, choose_mul_factorial_mul_factorial hkn,
         hp.multiplicity_factorial hnb, hp.multiplicity_mul,
-        hp.multiplicity_factorial ((log_le_log_of_le hkn).trans_lt hnb),
-        hp.multiplicity_factorial (lt_of_le_of_lt (log_le_log_of_le tsub_le_self) hnb),
+        hp.multiplicity_factorial ((log_mono_right hkn).trans_lt hnb),
+        hp.multiplicity_factorial (lt_of_le_of_lt (log_mono_right tsub_le_self) hnb),
         multiplicity_choose_aux hp hkn],
     simp [add_comm],
   end,
@@ -198,7 +198,7 @@ else if hn0 : n = 0 then by cases k; simp [hn0, *] at *
 else begin
   rw [multiplicity_choose hp (le_of_not_gt hkn) (lt_succ_self _),
     multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) (nat.pos_of_ne_zero hk0)
-      (lt_succ_of_le (log_le_log_of_le (le_of_not_gt hkn))),
+      (lt_succ_of_le (log_mono_right (le_of_not_gt hkn))),
     multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) (nat.pos_of_ne_zero hn0) (lt_succ_self _),
     ← nat.cast_add, enat.coe_le_coe],
   calc ((Ico 1 (log p n).succ).filter (λ i, p ^ i ∣ n)).card
@@ -226,7 +226,7 @@ le_antisymm
   begin
     rw [multiplicity_choose hp hkn (lt_succ_self _),
       multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0
-        (lt_succ_of_le (log_le_log_of_le hkn)),
+        (lt_succ_of_le (log_mono_right hkn)),
       ← nat.cast_add, enat.coe_le_coe, log_pow hp.one_lt,
       ← card_disjoint_union hdisj, filter_union_right],
     have filter_le_Ico := (Ico 1 n.succ).card_filter_le _,