case a
α : Type u_1
β : Type ?u.216947
γ : Type ?u.216950
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
x : α
⊢ x ∈ erase (erase s a) b ↔ x ∈ erase (erase s b) a
α : Type u_1
β : Type ?u.216947
γ : Type ?u.216950
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
⊢ erase (erase s a) b = erase (erase s b) a
ext x
case a
α : Type u_1
β : Type ?u.216947
γ : Type ?u.216950
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
x : α
⊢ (x ≠ b ∧ x ≠ a) ∧ x ∈ s ↔ (x ≠ a ∧ x ≠ b) ∧ x ∈ s
case a
α : Type u_1
β : Type ?u.216947
γ : Type ?u.216950
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
x : α
⊢ x ∈ erase (erase s a) b ↔ x ∈ erase (erase s b) a
simp only [mem_erase, ← and_assoc]
no goals
case a
α : Type u_1
β : Type ?u.216947
γ : Type ?u.216950
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
x : α
⊢ (x ≠ b ∧ x ≠ a) ∧ x ∈ s ↔ (x ≠ a ∧ x ≠ b) ∧ x ∈ s
rw [@and_comm (x ≠ a)]