u v : PrimeMultiset
h : PNat.factorMultiset (prod u) ≤ v ↔ prod u ∣ prod v := PNat.factorMultiset_le_iff'
⊢ prod u ∣ prod v ↔ u ≤ v
u v : PrimeMultiset
⊢ prod u ∣ prod v ↔ u ≤ v
let h := @PNat.factorMultiset_le_iff' u.prod v
u v : PrimeMultiset
h : u ≤ v ↔ prod u ∣ prod v
⊢ prod u ∣ prod v ↔ u ≤ v
u v : PrimeMultiset
h : PNat.factorMultiset (prod u) ≤ v ↔ prod u ∣ prod v := PNat.factorMultiset_le_iff'
⊢ prod u ∣ prod v ↔ u ≤ v
rw [u.factorMultiset_prod] at h
no goals
u v : PrimeMultiset
h : u ≤ v ↔ prod u ∣ prod v
⊢ prod u ∣ prod v ↔ u ≤ v
exact h.symm