-----Description-----  
his task requires writing a Lean 4 method decomposes a natural number `n` into its prime factorization components based on a user-provided list of primes. Specifically, it calculates the exponents for each prime in the factorization such that:
\[ n = \prod p^e \]
In other words, it determines the exponent e for each prime p.

-----Input-----
The input consists of:
- n: A positive natural number (n > 0) that can be expressed as a product of powers of the given primes.
- primes: A non-empty list of distinct prime numbers whose product of powers equals n.  

-----Output-----  
The output is `List (Nat × Nat)`:
Return a list of pair/Cartesian product of two natural numbers (p, e), where p is the prime and e is the exponent of p in the factorization. Each prime in the output must be from the input list, and every prime in the input list must appear in the output.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution
import Mathlib.Data.Nat.Prime.Defs
-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def findExponents_precond (n : Nat) (primes : List Nat) : Prop :=
  -- !benchmark @start precond
  n > 0 ∧
  primes.length > 0 ∧
  primes.all (fun p => Nat.Prime p) ∧
  List.Nodup primes
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def findExponents (n : Nat) (primes : List Nat) (h_precond : findExponents_precond (n) (primes)) : List (Nat × Nat) :=
  -- !benchmark @start code
  let rec countFactors (n : Nat) (primes : List Nat) : List (Nat × Nat) :=
    match primes with
    | [] => []
    | p :: ps =>
      let (count, n') :=
        countFactor n p 0
      (p, count) :: countFactors n' ps

  countFactors n primes
  where

  countFactor : Nat → Nat → Nat → Nat × Nat
  | 0, _, count =>
    (count, 0)
  | n, p, count =>
    if h : n > 0 ∧ p > 1 then
      have : n / p < n :=
        Nat.div_lt_self h.1 h.2
      if n % p == 0 then
        countFactor (n / p) p (count + 1)
      else
        (count, n)
    else
      (count, n)
  termination_by n _ _ => n
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def findExponents_postcond (n : Nat) (primes : List Nat) (result: List (Nat × Nat)) (h_precond : findExponents_precond (n) (primes)) : Prop :=
  -- !benchmark @start postcond
  (n = result.foldl (fun acc (p, e) => acc * p ^ e) 1) ∧
  result.all (fun (p, _) => p ∈ primes) ∧
  primes.all (fun p => result.any (fun pair => pair.1 = p))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem findExponents_spec_satisfied (n: Nat) (primes: List Nat) (h_precond : findExponents_precond (n) (primes)) :
    findExponents_postcond (n) (primes) (findExponents (n) (primes) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: n: 6
primes: [2, 3]
n: 6285195213566005335561053533150026217291776
primes: [2, 3, 5]
n: 360
primes: [2, 3, 5]
n: 18903812908
primes: [2, 43, 823, 133543]
n: 114514
primes: [2, 31, 1847]
n: 20241147794175
primes: [3, 5, 7, 11, 31, 47]
expected: [(2, 1), (3, 1)]
[(2, 55), (3, 55), (5, 0)]
[(2, 3), (3, 2), (5, 1)]
[(2, 2), (43, 1), (823, 1), (133543, 1)]
[(2, 1), (31, 1), (1847, 1)]
[(3, 3), (5, 2), (7, 1), (11, 3), (31, 1), (47, 3)]
unexpected: [(1, 2), (2, 3)]
[(2, 1), (3, 2)]
[(2, 2), (3, 55), (5, 59)]
[(2, 55), (3, 55), (7, 0)]
[(2, 3), (3, 2), (5, 0)]
[(2, 3), (3, 2), (7, 5)]
[(2, 2), (43, 4), (823, 0), (133543, 1)]
[(2, 2), (43, 1), (823, 2)]
[(2, 1), (31, 1), (1847, 0)]
[(2, 1), (33, 1), (1847, 1)]
[(0, 77), (17, 7)]
[(3, 3), (5, 2), (7, 1), (11, 3), (31, 1), (33, 2)]

Inputs rejected by the precondition:
n: 6
primes: [6]
n: 0
n: 0
primes: [2, 3]
n: 12
n: 12
primes: [2, 2, 3]