α : Type u_1
β : Type ?u.123926
γ : Type ?u.123929
inst✝ : DecidableEq α
s t : Finset α
x : α × α
h : _root_.Disjoint s t
⊢ Set.offDiag (↑s ∪ ↑t) = Set.offDiag ↑s ∪ Set.offDiag ↑t ∪ ↑s ×ˢ ↑t ∪ ↑t ×ˢ ↑s
α : Type u_1
β : Type ?u.123926
γ : Type ?u.123929
inst✝ : DecidableEq α
s t : Finset α
x : α × α
h : _root_.Disjoint s t
⊢ ↑(offDiag (s ∪ t)) = ↑(offDiag s ∪ offDiag t ∪ s ×ˢ t ∪ t ×ˢ s)
push_cast
no goals
α : Type u_1
β : Type ?u.123926
γ : Type ?u.123929
inst✝ : DecidableEq α
s t : Finset α
x : α × α
h : _root_.Disjoint s t
⊢ Set.offDiag (↑s ∪ ↑t) = Set.offDiag ↑s ∪ Set.offDiag ↑t ∪ ↑s ×ˢ ↑t ∪ ↑t ×ˢ ↑s
exact Set.offDiag_union (disjoint_coe.2 h)