feat(Tactic/Simproc/Divisors): add simprocs to compute the divisors of a natural number. (#27101)

This PR continues the work from #23026.

Original PR: #23026

Author: Paul-Lez

Mathlib.lean

@@ -5995,6 +5995,7 @@ import Mathlib.Tactic.Set
 import Mathlib.Tactic.SetLike
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.SimpRw
+import Mathlib.Tactic.Simproc.Divisors
 import Mathlib.Tactic.Simproc.ExistsAndEq
 import Mathlib.Tactic.Simproc.Factors
 import Mathlib.Tactic.Simps.Basic

Mathlib/Tactic.lean

@@ -248,6 +248,7 @@ import Mathlib.Tactic.Set
 import Mathlib.Tactic.SetLike
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.SimpRw
+import Mathlib.Tactic.Simproc.Divisors
 import Mathlib.Tactic.Simproc.ExistsAndEq
 import Mathlib.Tactic.Simproc.Factors
 import Mathlib.Tactic.Simps.Basic

Mathlib/Tactic/Simproc/Divisors.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Paul Lezeau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Lezeau, Bhavik Mehta
+-/
+import Mathlib.NumberTheory.Divisors
+import Mathlib.Util.Qq
+
+/-! # Divisor Simprocs
+
+This file implements (d)simprocs to compute various objects related to divisors:
+- `Nat.divisorsEq`: computes `Nat.divisors n` for explicit values of `n`
+- `Nat.properDivisorsEq`: computes `Nat.properDivisors n` for explicit values of `n`
+
+-/
+
+open Lean Meta Simp Qq
+
+/-- The `Nat.divisorsEq` computes the finset `Nat.divisors n` when `n` is a natural number
+literal. For instance, this simplifies `Nat.divisors 6` to `{1, 2, 3, 6}`. -/
+dsimproc_decl Nat.divisors_ofNat (Nat.divisors _) := fun e => do
+  unless e.isAppOfArity `Nat.divisors 1 do return .continue
+  let some n ← fromExpr? e.appArg! | return .continue
+  return .done <| mkSetLiteralQ q(Finset ℕ) <| ((unsafe n.divisors.val.unquot).map mkNatLit)
+
+/-- Compute the finset `Nat.properDivisorsEq n` when `n` is a numeral.
+For instance, this simplifies `Nat.properDivisorsEq 12` to `{1, 2, 3, 4, 6}`. -/
+dsimproc_decl Nat.properDivisors_ofNat (Nat.properDivisors _) := fun e => do
+  unless e.isAppOfArity `Nat.properDivisors 1 do return .continue
+  let some n ← fromExpr? e.appArg! | return .continue
+  return unsafe .done <| mkSetLiteralQ q(Finset ℕ) <|
+    ((unsafe n.properDivisors.val.unquot).map mkNatLit)

MathlibTest/Simproc/Divisors.lean

@@ -0,0 +1,42 @@
+import Mathlib.Tactic.Simproc.Divisors
+import Mathlib.NumberTheory.Primorial
+
+open Nat
+
+example :
+    Nat.divisors 1710 = {1, 2, 3, 5, 6, 9, 10, 15, 18, 19, 30, 38, 45, 57,
+      90, 95, 114, 171, 190, 285, 342, 570, 855, 1710} := by
+  simp only [Nat.divisors_ofNat]
+
+example : Nat.divisors 57 = {1, 3, 19, 57} := by
+  simp only [Nat.divisors_ofNat]
+
+example : (Nat.divisors <| 6 !).card = 30 := by
+  simp [Nat.divisors_ofNat, Nat.factorial_succ]
+
+example : (Nat.divisors <| primorial 12).card = 32 := by
+  --TODO(Paul-Lez): seems like we need a norm_num extension for computing `primorial`!
+  have : primorial 12 = 2310 := rfl
+  simp [Nat.divisors_ofNat, this]
+
+example : (Nat.divisors <| 2^13).card = 14 := by
+  simp [Nat.divisors_ofNat]
+
+example : 2 ≤ Finset.card (Nat.divisors 3) := by
+  simp [Nat.divisors_ofNat]
+
+/-- error: simp made no progress -/
+#guard_msgs in
+example (n : ℕ) (hn : n ≠ 0) : 1 ≤ Finset.card (Nat.divisors n) := by
+  simp only [Nat.divisors_ofNat]
+
+example :
+    Nat.properDivisors 1710 = {1, 2, 3, 5, 6, 9, 10, 15, 18, 19, 30, 38, 45, 57,
+      90, 95, 114, 171, 190, 285, 342, 570, 855} := by
+  simp only [Nat.properDivisors_ofNat]
+
+example : Nat.properDivisors 57 = {1, 3, 19} := by
+  simp only [Nat.properDivisors_ofNat]
+
+example : 2 ≤ Finset.card (Nat.divisors 3) := by
+  simp [Nat.divisors_ofNat]