α : Type u_1
s t : Set α
x✝ : α × α
a : α
x : α × α
⊢ (x.fst ∈ s ∧ x.fst ∈ t) ∧ (x.snd ∈ s ∧ x.snd ∈ t) ∧ x.fst ≠ x.snd ↔
    (x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd) ∧ x.fst ∈ t ∧ x.snd ∈ t ∧ x.fst ≠ x.snd
α : Type u_1
s t : Set α
x✝ : α × α
a : α
x : α × α
⊢ x ∈ offDiag (s ∩ t) ↔ x ∈ offDiag s ∩ offDiag t
simp only [mem_offDiag, mem_inter_iff]
no goals
α : Type u_1
s t : Set α
x✝ : α × α
a : α
x : α × α
⊢ (x.fst ∈ s ∧ x.fst ∈ t) ∧ (x.snd ∈ s ∧ x.snd ∈ t) ∧ x.fst ≠ x.snd ↔
    (x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd) ∧ x.fst ∈ t ∧ x.snd ∈ t ∧ x.fst ≠ x.snd
tauto