case a
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m ⊓ factorMultiset n

case a
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset (gcd m n)
m n : ℕ+
⊢ factorMultiset (gcd m n) = factorMultiset m ⊓ factorMultiset n
apply le_antisymm
case a
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m ∧ factorMultiset (gcd m n) ≤ factorMultiset n
case a
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m ⊓ factorMultiset n
apply le_inf_iff.mpr
case a.left
m n : ℕ+
⊢ gcd m n ∣ m

case a.right
m n : ℕ+
⊢ gcd m n ∣ n
case a
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m ∧ factorMultiset (gcd m n) ≤ factorMultiset n
constructor <;> apply factorMultiset_le_iff.mpr
case a.right
m n : ℕ+
⊢ gcd m n ∣ n
case a.left
m n : ℕ+
⊢ gcd m n ∣ m

case a.right
m n : ℕ+
⊢ gcd m n ∣ n
exact gcd_dvd_left m n
no goals
case a.right
m n : ℕ+
⊢ gcd m n ∣ n
exact gcd_dvd_right m n
case a
m n : ℕ+
⊢ PrimeMultiset.prod (factorMultiset m ⊓ factorMultiset n) ∣ gcd m n
case a
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset (gcd m n)
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
case a.hm
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset m

case a.hn
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset n
case a
m n : ℕ+
⊢ PrimeMultiset.prod (factorMultiset m ⊓ factorMultiset n) ∣ gcd m n
apply dvd_gcd <;> rw [PrimeMultiset.prod_dvd_iff']
case a.hn
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset n
case a.hm
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset m

case a.hn
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset n
exact inf_le_left
no goals
case a.hn
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset n
exact inf_le_right