case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0

case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0
n m : ℕ
⊢ n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0
rcases eq_or_ne m 0 with (rfl | hm)
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∣ m → n ≤ m
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0
simp only [hm, Ne.def, not_false_iff, and_true_iff, ← filter_dvd_eq_divisors hm, mem_filter,
  mem_range, and_iff_right_iff_imp, lt_succ_iff]
no goals
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∣ m → n ≤ m
exact le_of_dvd hm.bot_lt
no goals
case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0
simp [divisors]