case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0

case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ properDivisors m ↔ n ∣ m ∧ n < m
n m : ℕ
⊢ n ∈ properDivisors m ↔ n ∣ m ∧ n < m
rcases eq_or_ne m 0 with (rfl | hm)
no goals
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ properDivisors m ↔ n ∣ m ∧ n < m
simp only [and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range]
no goals
case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0
simp [properDivisors]