no goals
F : Type ?u.606313
α : Type u_1
β : Type ?u.606319
γ : Type ?u.606322
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t
rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]