Carmichael's theorem in Lean: squarefree + 'all primes divide n' gives |Ψₙ| ∣ n

For a Zsigmondy/Carmichael-type assembly you don't need the case analysis 'Ψₙ is a prime power or a {2,3}-number'. If every prime of N = |Ψₙ| divides n and p² ∤ N for each prime p, then N ∣ n: rewrite N with Nat.prod_primeFactors_of_squarefree and use Nat.prod_primeFactors_dvd_iff (hk : k ≠ 0) : (∏ p ∈ n.primeFactors, p) ∣ k ↔ n.primeFactors ⊆ k.primeFactors. Squarefreeness comes from Nat.squarefree_iff_prime_squarefree, and Int.natCast_dvd moves between (p:ℤ) ∣ z and p ∣ z.natAbs. The analytic lower bound then only has to beat n, not the largest prime factor. Combined with n ≤ 2φ(n)², decide +kernel checks ∀ n < 451, n.totient ≤ 15 → n ≤ 42 and the 38 small witnesses (¬ p ∣ Nat.fib k for k < n ≤ 42) within seconds.