reverse orders in finset filter

Stream: new members

[Emma R. Hasson]

Can anyone help with this? We seem to need to break it into sums and then use sum_comm, but feel there should be a more direct route.

example (P : ℕ → ℕ → Prop) (s t : finset ℕ) :
∑ (a:ℕ×ℕ) in finset.filter (λ (x : ℕ×ℕ), P x.1  x.2) (s.product t), 1  =
∑ (a:ℕ×ℕ) in finset.filter (λ (x : ℕ×ℕ), P x.2  x.1) (t.product s), 1 :=
begin
 sorry,
end

[Kenny Lau]

you could observe that this equality is induced by a bijection of the domain

[Yakov Pechersky]

import algebra.big_operators.basic

open_locale big_operators
open finset


example (P : ℕ → ℕ → Prop) [∀ x y, decidable (P x y)] (s t : finset ℕ) :
  ∑ (a:ℕ×ℕ) in filter (λ (x : ℕ×ℕ), P x.1  x.2) (s.product t), 1  =
  ∑ (a:ℕ×ℕ) in filter (λ (x : ℕ×ℕ), P x.2  x.1) (t.product s), 1 :=
begin
  refine sum_bij (λ a _, a.swap) _ (λ _ _, rfl) (λ _ _ _ _, prod.swap_inj.mp) _,
  { rintro ⟨⟩,
    simp {contextual := tt} },
  { rintro ⟨x, y⟩ h,
    refine ⟨(y, x), _, rfl⟩,
    simpa [and.comm] using h }
end

[Eric Wieser]

Sounds like we're missing the lemma that says (s.product t).map equiv.prod_comm.to_embedding = t.product s

[Yaël Dillies]

docs#set.image_swap_prod for the set version.