case a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.23162
s s' : Finset α
t t' : Finset β
a✝ : α
b✝ : β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ↔ (a, b) ∈ filter p s ×ˢ filter q t
α : Type u_1
β : Type u_2
γ : Type ?u.23162
s s' : Finset α
t t' : Finset β
a : α
b : β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) = filter p s ×ˢ filter q t
ext ⟨a, b⟩
no goals
case a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.23162
s s' : Finset α
t t' : Finset β
a✝ : α
b✝ : β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.fst ∧ q x.snd) (s ×ˢ t) ↔ (a, b) ∈ filter p s ×ˢ filter q t
simp [mem_filter, mem_product, decide_eq_true_eq, and_comm, and_left_comm, and_assoc]