α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
a : α × α
h : a ∈ offDiag s
⊢ ¬a.fst = a.snd
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
a : α × α
h : a ∈ offDiag s
⊢ ¬Sym2.IsDiag (Quotient.mk (Sym2.Rel.setoid α) a)
rw [Sym2.isDiag_iff_proj_eq]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
a : α × α
h : a ∈ offDiag s
⊢ ¬a.fst = a.snd
exact (mem_offDiag.1 h).2.2