α : Type u_1
β : Type ?u.122500
γ : Type ?u.122503
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ Set.offDiag (↑s ∩ ↑t) = Set.offDiag ↑s ∩ Set.offDiag ↑t
α : Type u_1
β : Type ?u.122500
γ : Type ?u.122503
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ ↑(offDiag (s ∩ t)) = ↑(offDiag s ∩ offDiag t)
push_cast
no goals
α : Type u_1
β : Type ?u.122500
γ : Type ?u.122503
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ Set.offDiag (↑s ∩ ↑t) = Set.offDiag ↑s ∩ Set.offDiag ↑t
exact Set.offDiag_inter _ _