simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at *
case right.mk.mk
a : ℕ
ha : a ∈ {1, 2, 6, 30, 210}
b : ℕ
hb : b ∈ {1, 2, 6, 30, 210}
⊢ a ∣ b ∨ b ∣ a
case right.mk.mk
a b : ℕ
ha : a = 1 ∨ a = 2 ∨ a = 6 ∨ a = 30 ∨ a = 210
hb : b = 1 ∨ b = 2 ∨ b = 6 ∨ b = 30 ∨ b = 210
⊢ a ∣ b ∨ b ∣ a