rw [hmul]
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree (m / l * l)
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree m