case a
m n : ℕ+
⊢ factorMultiset (lcm m n) ≤ factorMultiset m ⊔ factorMultiset n

case a
m n : ℕ+
⊢ factorMultiset m ⊔ factorMultiset n ≤ factorMultiset (lcm m n)
m n : ℕ+
⊢ factorMultiset (lcm m n) = factorMultiset m ⊔ factorMultiset n
apply le_antisymm
case a
m n : ℕ+
⊢ lcm m n ∣ PrimeMultiset.prod (factorMultiset m ⊔ factorMultiset n)
case a
m n : ℕ+
⊢ factorMultiset (lcm m n) ≤ factorMultiset m ⊔ factorMultiset n
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
case a.hm
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset m ⊔ factorMultiset n

case a.hn
m n : ℕ+
⊢ factorMultiset n ≤ factorMultiset m ⊔ factorMultiset n
case a
m n : ℕ+
⊢ lcm m n ∣ PrimeMultiset.prod (factorMultiset m ⊔ factorMultiset n)
apply lcm_dvd <;> rw [← factorMultiset_le_iff']
case a.hn
m n : ℕ+
⊢ factorMultiset n ≤ factorMultiset m ⊔ factorMultiset n
case a.hm
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset m ⊔ factorMultiset n

case a.hn
m n : ℕ+
⊢ factorMultiset n ≤ factorMultiset m ⊔ factorMultiset n
exact le_sup_left
no goals
case a.hn
m n : ℕ+
⊢ factorMultiset n ≤ factorMultiset m ⊔ factorMultiset n
exact le_sup_right
case a
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset (lcm m n) ∧ factorMultiset n ≤ factorMultiset (lcm m n)
case a
m n : ℕ+
⊢ factorMultiset m ⊔ factorMultiset n ≤ factorMultiset (lcm m n)
apply sup_le_iff.mpr
case a.left
m n : ℕ+
⊢ m ∣ lcm m n

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

case a.right
m n : ℕ+
⊢ n ∣ lcm m n
exact dvd_lcm_left m n
no goals
case a.right
m n : ℕ+
⊢ n ∣ lcm m n
exact dvd_lcm_right m n