α : Type u_1
β : Type ?u.207977
γ : Type ?u.207980
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s
α : Type u_1
β : Type ?u.207977
γ : Type ?u.207980
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ∈ erase s b
simp only [mem_erase]
no goals
α : Type u_1
β : Type ?u.207977
γ : Type ?u.207980
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s
exact And.intro