rw [←h] at hd
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
h : l = d
⊢ False
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : l ∈ m.divisors
h : l = d
⊢ False