Counting divisors

Stream: lean4

[Janitha]

import Mathlib
open Nat
set_option exponentiation.threshold 5000

/- How many positive integer divisors of
   2004^{2004} are divisible by exactly 2004 positive integers? -/
example :
  {x : ℕ | x > 0 ∧ x ∣ 2004^2004 ∧ {k | k > 0 ∧ k ∣ x}.encard = 2004}.encard = 54 := by

  -- Prime factorization of 2004
  have h_factorization : 2004 = 2^2 * 3 * 167 := by norm_num

  -- Prime factorization of 2004^2004
  have h_exp_factorization : 2004^2004 = 2^(2*2004) * 3^2004 * 167^2004 := by
    rw [h_factorization, pow_mul, pow_mul, pow_mul]
    norm_num

  -- A divisor of 2004^2004 has the form 2^a * 3^b * 167^c
  let validDivisors := {x : ℕ | ∃ a b c : ℕ, x = 2^a * 3^b * 167^c ∧ x ∣ 2004^2004 ∧ {k | k > 0 ∧ k ∣ x}.encard = 2004}

  -- The count condition
  have h_equiv_sets :
    {x | x > 0 ∧ x ∣ 2004^2004 ∧ {k | k > 0 ∧ k ∣ x}.encard = 2004} = validDivisors := by

    ext x
    simp only [validDivisors]
    constructor
    · rintro ⟨hx_pos, hx_dvd, hx_card⟩ -- x>0, x∣2004^2004, cardinality of set of k's dividing x = 2004
      obtain ⟨a, b, c, rfl⟩ : ∃ a b c, x = 2^a * 3^b * 167^c := by
        rw [h_exp_factorization] at hx_dvd
        --exact Nat.factors_unique hx_dvd
        sorry
      exact ⟨a, b, c, rfl, hx_dvd, hx_card⟩
    · rintro ⟨a, b, c, rfl, hx_dvd, hx_card⟩
      --exact ⟨Nat.pos_of_ne_zero (pow_ne_zero _ Nat.two_ne_zero), hx_dvd, hx_card⟩
      sorry

  --Counting valid (a, b, c) solutions
  have h_count : { (a, b, c) | (a + 1) * (b + 1) * (c + 1) = 2004 }.encard = 54 := by
    -- Factorizing 2004
    have h_factorization : 2004 = 2^2 * 3 * 167 := by norm_num

  -- Number of ways to partition the exponent of 2 (4 = 2 + 1 + 1, order matters)
    have h_partition_2s : Nat.choose 4 2 = 6 := by rfl
  -- Number of ways to distribute the factor 3 (assigning 1,1,1 among (b+1),(c+1),(d+1))
    have h_partition_3 : 3 = 3 := by rfl
  -- Number of ways to distribute the factor 167
    have h_partition_167 : 3 = 3 := by rfl
  -- Compute total count: 6 * 3 * 3 = 54
    have h_total_count : 6 * 3 * 3 = 54 := by rfl
  -- Conclude
    sorry

  /- Establishing the final result -/
  have h_final : validDivisors.encard = 54 := by
    simp [validDivisors, h_count]
    sorry


  rw [← h_equiv_sets] at h_final
  exact h_final

I'm having trouble filling the first two sorry's. Couldn't find the correct theorem/lemma. Please help.

[Notification Bot]

Janitha has marked this topic as resolved.

[Notification Bot]

Jeremy Tan has marked this topic as unresolved.

[Jeremy Tan]

:question:

[Aaron Liu]

import Mathlib
open Nat
set_option exponentiation.threshold 5000

/- How many positive integer divisors of
   2004^{2004} are divisible by exactly 2004 positive integers? -/
example :
  {x : ℕ | x > 0 ∧ x ∣ 2004^2004 ∧ {k | k > 0 ∧ k ∣ x}.encard = 2004}.encard = 54 := by

  -- Prime factorization of 2004
  have h_factorization : 2004 = 2^2 * 3 * 167 := by norm_num

  -- Prime factorization of 2004^2004
  have h_exp_factorization : 2004^2004 = 2^(2*2004) * 3^2004 * 167^2004 := by
    rw [h_factorization, pow_mul, pow_mul, pow_mul]
    norm_num

  -- A divisor of 2004^2004 has the form 2^a * 3^b * 167^c
  let validDivisors := {x : ℕ | ∃ a b c : ℕ, x = 2^a * 3^b * 167^c ∧ x ∣ 2004^2004 ∧ {k | k > 0 ∧ k ∣ x}.encard = 2004}

  -- The count condition
  have h_equiv_sets :
    {x | x > 0 ∧ x ∣ 2004^2004 ∧ {k | k > 0 ∧ k ∣ x}.encard = 2004} = validDivisors := by

    ext x
    simp only [validDivisors]
    constructor
    · rintro ⟨hx_pos, hx_dvd, hx_card⟩ -- x>0, x∣2004^2004, cardinality of set of k's dividing x = 2004
      obtain ⟨a, b, c, rfl⟩ : ∃ a b c, x = 2^a * 3^b * 167^c := by
        rw [h_exp_factorization] at hx_dvd
        --exact Nat.factors_unique hx_dvd
        rw [Nat.dvd_mul] at hx_dvd
        obtain ⟨y, z, hy, hz, rfl⟩ := hx_dvd
        rw [Nat.dvd_mul] at hy
        obtain ⟨x, y, hx, hy, rfl⟩ := hy
        rw [Nat.dvd_prime_pow (by norm_num)] at hx hy hz
        obtain ⟨x, _, rfl⟩ := hx
        obtain ⟨y, _, rfl⟩ := hy
        obtain ⟨z, _, rfl⟩ := hz
        use x, y, z
      exact ⟨a, b, c, rfl, hx_dvd, hx_card⟩
    · rintro ⟨a, b, c, rfl, hx_dvd, hx_card⟩
      --exact ⟨Nat.pos_of_ne_zero (pow_ne_zero _ Nat.two_ne_zero), hx_dvd, hx_card⟩
      exact ⟨by positivity, hx_dvd, hx_card⟩

  --Counting valid (a, b, c) solutions
  have h_count : { (a, b, c) | (a + 1) * (b + 1) * (c + 1) = 2004 }.encard = 54 := by
    -- Factorizing 2004
    have h_factorization : 2004 = 2^2 * 3 * 167 := by norm_num

  -- Number of ways to partition the exponent of 2 (4 = 2 + 1 + 1, order matters)
    have h_partition_2s : Nat.choose 4 2 = 6 := by rfl
  -- Number of ways to distribute the factor 3 (assigning 1,1,1 among (b+1),(c+1),(d+1))
    have h_partition_3 : 3 = 3 := by rfl
  -- Number of ways to distribute the factor 167
    have h_partition_167 : 3 = 3 := by rfl
  -- Compute total count: 6 * 3 * 3 = 54
    have h_total_count : 6 * 3 * 3 = 54 := by rfl
  -- Conclude
    sorry

  /- Establishing the final result -/
  have h_final : validDivisors.encard = 54 := by
    simp [validDivisors, h_count]
    sorry


  rw [← h_equiv_sets] at h_final
  exact h_final

[Janitha]

Thanks Aaron!