big_operators and bijections

Stream: Is there code for X?

[Heather Macbeth]

I would like to use the fact that one can pull back a sum over a fintype under a bijection. I can prove this as follows:

lemma sum_bij'' {α : Type*} {β : Type*} {γ : Type*} [add_comm_monoid β] [fintype α] [fintype γ]
  {g : γ → β} (i : α → γ) (i_inj : injective i) (i_surj : surjective i) :
  (∑ x, g (i x)) = (∑ x, g x) :=
begin
  refine finset.sum_bij _ _ _ (λ a₁ a₂ _ _ , @i_inj a₁ a₂) _,
  { simp },
  { simp },
  { intros b _,
    obtain ⟨a, ha⟩ := @i_surj b,
    exact ⟨a, finset.mem_univ a, ha.symm⟩ },
end

[Heather Macbeth]

As one can see, the key point of the proof is docs#finset.sum_bij. I found the hypotheses there quite hard to check, which is why I wrote my own lemma (for now -- not sure whether it's appropriate for a PR).

[Heather Macbeth]

But I was wondering if I am missing some folk wisdom on how to use a lemma like this docs#finset.sum_bij neatly.

[Heather Macbeth]

For example, the "surjectivity" hypothesis on that lemma is

∀ (b : γ), b ∈ t → (∃ (a : α) (ha : a ∈ s), b = i a ha)

Is there a cleaner way of deducing this from surjective i than what I wrote?

[Heather Macbeth]

And perhaps more generally, docs#finset.sum_bij is written for a strange object of type Π (a : α), a ∈ s → γ -- effectively a partially defined function. I can see why that choice is made, but how do I turn my actual function i into an object like this?

[Johan Commelin]

I think there is also sum_equiv

[Johan Commelin]

Let me search a bit

[Johan Commelin]

Test: docs#equiv.sum_comp

[Johan Commelin]

@Heather Macbeth If you upgrade your map i to an equiv then you're done by that lemma.

[Heather Macbeth]

Great! Thank you! Actually my map was already an equiv, I downgraded it to try to match the other lemma :)