m : ℕ+
v : PrimeMultiset
h : factorMultiset m ≤ factorMultiset (PrimeMultiset.prod v) ↔ m ∣ PrimeMultiset.prod v := factorMultiset_le_iff
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
m : ℕ+
v : PrimeMultiset
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
let h := @factorMultiset_le_iff m v.prod
m : ℕ+
v : PrimeMultiset
h : factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
m : ℕ+
v : PrimeMultiset
h : factorMultiset m ≤ factorMultiset (PrimeMultiset.prod v) ↔ m ∣ PrimeMultiset.prod v := factorMultiset_le_iff
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
rw [v.factorMultiset_prod] at h
no goals
m : ℕ+
v : PrimeMultiset
h : factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
exact h