no goals
α : Type u_1
β : Type ?u.121780
γ : Type ?u.121783
inst✝ : DecidableEq α
s t : Finset α
x✝ x : α × α
⊢ x ∈ diag (s ∩ t) ↔ x ∈ diag s ∩ diag t
simpa only [mem_diag, mem_inter] using and_and_right