α : Type u_1
β : Type ?u.217477
γ : Type ?u.217480
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ (∀ ⦃x : α⦄, x ∈ s → ¬x = a → x ∈ t) ↔ ∀ ⦃x : α⦄, x ≠ a → x ∈ s → x ∈ t
α : Type u_1
β : Type ?u.217477
γ : Type ?u.217480
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ s ⊆ insert a t ↔ erase s a ⊆ t
simp only [subset_iff, or_iff_not_imp_left, mem_erase, mem_insert, and_imp]
no goals
α : Type u_1
β : Type ?u.217477
γ : Type ?u.217480
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ (∀ ⦃x : α⦄, x ∈ s → ¬x = a → x ∈ t) ↔ ∀ ⦃x : α⦄, x ≠ a → x ∈ s → x ∈ t
exact forall_congr' fun x => forall_swap