feat: add strictMono_mersenne and corollaries (#12687)

Incl. upgrade of `mersenne_pos` to an `Iff`.

Also add a `positivity` extension and use it in a few lemmas.

Author: urkud

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -53,8 +53,7 @@ theorem perfect_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1))
       (Nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)),
     sigma_two_pow_eq_mersenne_succ]
   · simp [pr, Nat.prime_two, sigma_one_apply]
-  · apply mul_pos (pow_pos _ k) (mersenne_pos (Nat.succ_pos k))
-    norm_num
+  · positivity
 #align theorems_100.nat.perfect_two_pow_mul_mersenne_of_prime Theorems100.Nat.perfect_two_pow_mul_mersenne_of_prime
 
 theorem ne_zero_of_prime_mersenne (k : ℕ) (pr : (mersenne (k + 1)).Prime) : k ≠ 0 := by
@@ -94,7 +93,7 @@ theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n) (p
       (Nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)) (Dvd.intro _ perf) with
     ⟨j, rfl⟩
   rw [← mul_assoc, mul_comm _ (mersenne _), mul_assoc] at perf
-  have h := mul_left_cancel₀ (ne_of_gt (mersenne_pos (Nat.succ_pos _))) perf
+  have h := mul_left_cancel₀ (by positivity) perf
   rw [sigma_one_apply, Nat.sum_divisors_eq_sum_properDivisors_add_self, ← succ_mersenne, add_mul,
     one_mul, add_comm] at h
   have hj := add_left_cancel h

Mathlib/NumberTheory/LucasLehmer.lean

@@ -43,17 +43,49 @@ def mersenne (p : ℕ) : ℕ :=
   2 ^ p - 1
 #align mersenne mersenne
 
-theorem mersenne_pos {p : ℕ} (h : 0 < p) : 0 < mersenne p := by
-  dsimp [mersenne]
-  calc
-    0 < 2 ^ 1 - 1 := by norm_num
-    _ ≤ 2 ^ p - 1 := Nat.sub_le_sub_right (Nat.pow_le_pow_of_le_right (Nat.succ_pos 1) h) 1
+theorem strictMono_mersenne : StrictMono mersenne := fun m n h ↦
+  (Nat.sub_lt_sub_iff_right <| Nat.one_le_pow _ _ two_pos).2 <| by gcongr; norm_num1
+
+@[simp]
+theorem mersenne_lt_mersenne {p q : ℕ} : mersenne p < mersenne q ↔ p < q :=
+  strictMono_mersenne.lt_iff_lt
+
+@[gcongr] protected alias ⟨_, GCongr.mersenne_lt_mersenne⟩ := mersenne_lt_mersenne
+
+@[simp]
+theorem mersenne_le_mersenne {p q : ℕ} : mersenne p ≤ mersenne q ↔ p ≤ q :=
+  strictMono_mersenne.le_iff_le
+
+@[gcongr] protected alias ⟨_, GCongr.mersenne_le_mersenne⟩ := mersenne_le_mersenne
+
+@[simp] theorem mersenne_zero : mersenne 0 = 0 := rfl
+
+@[simp] theorem mersenne_pos {p : ℕ} : 0 < mersenne p ↔ 0 < p := mersenne_lt_mersenne (p := 0)
 #align mersenne_pos mersenne_pos
 
-theorem one_lt_mersenne {p : ℕ} (hp : 1 < p) : 1 < mersenne p :=
-  lt_tsub_iff_right.2 <|
-    calc 1 + 1 = 2 ^ 1 := by rw [one_add_one_eq_two, pow_one]
-    _ < 2 ^ p := pow_lt_pow_right one_lt_two hp
+namespace Mathlib.Meta.Positivity
+
+open Lean Meta Qq Function
+
+alias ⟨_, mersenne_pos_of_pos⟩ := mersenne_pos
+
+/-- Extension for the `positivity` tactic: `mersenne`. -/
+@[positivity mersenne _]
+def evalMersenne : PositivityExt where eval {u α} _zα _pα e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(mersenne $a) =>
+    let ra ← core q(inferInstance) q(inferInstance) a
+    assertInstancesCommute
+    match ra with
+    | .positive pa => pure (.positive q(mersenne_pos_of_pos $pa))
+    | _ => pure (.nonnegative q(Nat.zero_le (mersenne $a)))
+  | _, _, _ => throwError "not mersenne"
+
+end Mathlib.Meta.Positivity
+
+@[simp]
+theorem one_lt_mersenne {p : ℕ} : 1 < mersenne p ↔ 1 < p :=
+  mersenne_lt_mersenne (p := 1)
 
 @[simp]
 theorem succ_mersenne (k : ℕ) : mersenne k + 1 = 2 ^ k := by
@@ -415,7 +447,7 @@ Here and below, we introduce `p' = p - 2`, in order to avoid using subtraction i
 
 /-- If `1 < p`, then `q p`, the smallest prime factor of `mersenne p`, is more than 2. -/
 theorem two_lt_q (p' : ℕ) : 2 < q (p' + 2) := by
-  refine (minFac_prime (one_lt_mersenne ?_).ne').two_le.lt_of_ne' ?_
+  refine (minFac_prime (one_lt_mersenne.2 ?_).ne').two_le.lt_of_ne' ?_
   · exact le_add_left _ _
   · rw [Ne, minFac_eq_two_iff, mersenne, Nat.pow_succ']
     exact Nat.two_not_dvd_two_mul_sub_one Nat.one_le_two_pow
@@ -527,7 +559,7 @@ theorem lucas_lehmer_sufficiency (p : ℕ) (w : 1 < p) : LucasLehmerTest p → (
   rw [z] at a
   rw [z] at t
   have h₁ := order_ineq p' t
-  have h₂ := Nat.minFac_sq_le_self (mersenne_pos (Nat.lt_of_succ_lt w)) a
+  have h₂ := Nat.minFac_sq_le_self (mersenne_pos.2 (Nat.lt_of_succ_lt w)) a
   have h := lt_of_lt_of_le h₁ h₂
   exact not_lt_of_ge (Nat.sub_le _ _) h
 #align lucas_lehmer_sufficiency lucas_lehmer_sufficiency