no goals
α : Type u_1
β : Type ?u.994
γ : Type ?u.997
s✝ t s : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑(offDiag s)
⊢ ∀ (a : α × α), a ∈ toFinset (offDiag s) ↔ a ∈ Finset.offDiag (toFinset s)
simp