case a
α : Type u_1
β : Type ?u.224919
γ : Type ?u.224922
inst✝ : DecidableEq α
s✝ t✝ u✝ v : Finset α
a b : α
s t u : Finset α
x : α
⊢ x ∈ s ∩ (t \ u) ↔ x ∈ (s ∩ t) \ u
α : Type u_1
β : Type ?u.224919
γ : Type ?u.224922
inst✝ : DecidableEq α
s✝ t✝ u✝ v : Finset α
a b : α
s t u : Finset α
⊢ s ∩ (t \ u) = (s ∩ t) \ u
ext x
no goals
case a
α : Type u_1
β : Type ?u.224919
γ : Type ?u.224922
inst✝ : DecidableEq α
s✝ t✝ u✝ v : Finset α
a b : α
s t u : Finset α
x : α
⊢ x ∈ s ∩ (t \ u) ↔ x ∈ (s ∩ t) \ u
simp [and_assoc]