Theorem: Aux.gcd_dvd_mul (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
m n : ℕ
⊢ m.gcd n ∣ m * n
Tactic:
calc
  m.gcd n ∣ m := Nat.gcd_dvd_left m n
  _ ∣ m * n := ⟨n, rfl⟩
State after:
no goals