α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ (∃ a, a ∈ s ×ˢ s ∧ Quotient.mk' a = m) → ∀ (a : α), a ∈ m → a ∈ s
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ m ∈ Finset.sym2 s ↔ ∀ (a : α), a ∈ m → a ∈ s
refine
  mem_image.trans
    ⟨?_, fun h ↦ ⟨m.out, mem_product.2 ⟨h _ m.out_fst_mem, h _ m.out_snd_mem⟩, m.out_eq⟩⟩
case intro.mk.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ a b : α
h : (a, b) ∈ s ×ˢ s
⊢ ∀ (a_1 : α), a_1 ∈ Quotient.mk' (a, b) → a_1 ∈ s
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ (∃ a, a ∈ s ×ˢ s ∧ Quotient.mk' a = m) → ∀ (a : α), a ∈ m → a ∈ s
rintro ⟨⟨a, b⟩, h, rfl⟩
case intro.mk.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ a b : α
h : (a, b) ∈ s ×ˢ s
⊢ a ∈ s ∧ b ∈ s
case intro.mk.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ a b : α
h : (a, b) ∈ s ×ˢ s
⊢ ∀ (a_1 : α), a_1 ∈ Quotient.mk' (a, b) → a_1 ∈ s
rw [Quotient.mk', @Sym2.ball _ (fun x ↦ x ∈ s)]
no goals
case intro.mk.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ a b : α
h : (a, b) ∈ s ×ˢ s
⊢ a ∈ s ∧ b ∈ s
rwa [mem_product] at h