n divides pq means n is 1 or p or q or pq

Stream: Is there code for X?

[Sabbir Rahman]

Just as title says, is there a code for n dividing pq with prime p, q implies n is one of of 1, p, q, or pq?

I have proven it, but seems like a simple fact that I don't want to repeat

[Sabbir Rahman]

at the same time, if there is none, any shorter proof then this?

import Mathlib

example (p q n : ℕ) (hp: Nat.Prime p) (hq: Nat.Prime q) (hnpq : n ∣ p * q) : n = 1 ∨ n = p ∨ n = q ∨ n = p*q := by
  obtain h | h := @or_not (p ∣ n)
  . have : (n:ℤ) / p ∣ p * q / p := Int.ediv_dvd_ediv (by norm_cast) (by norm_cast)
    norm_cast at this
    rw [Nat.mul_div_right _ (by exact Nat.Prime.pos hp)] at this
    obtain h' | h' := (Nat.dvd_prime hq).mp this <;> simp [Nat.eq_mul_of_div_eq_right h h']
  . have : Nat.Coprime p n := by exact (Nat.Prime.coprime_iff_not_dvd hp).mpr h
    have : n ∣ q := by exact Nat.Coprime.dvd_of_dvd_mul_left (Nat.coprime_comm.mp this) hnpq
    obtain h' | h' := (Nat.dvd_prime hq).mp this <;> simp [h']

[Aaron Liu]

import Mathlib.RingTheory.UniqueFactorizationDomain.Nat

example (p q n : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) :
    n ∣ p * q ↔ n = 1 ∨ n = p ∨ n = q ∨ n = p * q := by
  simp only [dvd_mul, Nat.dvd_prime, hp, hq, and_or_left, or_and_right,
    exists_or, exists_and_left, exists_eq_left, one_mul, mul_one]
  tauto

[Edison Xie]

example (p q n : ℕ) (hp: Nat.Prime p) (hq: Nat.Prime q) :
    n ∣ p * q ↔ n = 1 ∨ n = p ∨ n = q ∨ n = p*q := by
  simp_all only [dvd_mul, Nat.dvd_prime]; aesop