How to reorder the sum of Finset?

Stream: Is there code for X?

[Lingwei Peng (彭灵伟)]

This is an IMO problem, and I’ve completed most of the proof. However, I left one sorry at h_eq, which is related to reordering the sum over a Finset. Could you help me figure out how to handle that part?

import Mathlib

theorem h_eq (n : ℕ) (n_pos : 0 < n) (a : ℕ → ℝ) (ha : ∀ i, a i ∈ Set.Icc 1 8)
  (M : Finset ℕ) (hM : M = (Finset.range n).filter (fun i => a i ∈ Set.Ioc 2 4))
: ∑ i ∈ M, ((Finset.filter (fun l => l ∈ M) (Finset.range (i + 1))).card)
  = ∑ i ∈ Finset.range (M.card), (i + 1) := by
  sorry

[Yaël Dillies]

Can you provide a #mwe ? I don't see what part of your code I am supposed to be looking at

[Yaël Dillies]

Probably you want something like docs#Finset.sum_nbij

[Lingwei Peng (彭灵伟)]

(deleted)

[Lingwei Peng (彭灵伟)]

(deleted)

[Lingwei Peng (彭灵伟)]

@Yaël Dillies Hey! I’ve cleaned up the problem description a bit. Is this #mwe okay with you?

[Edison Xie]

I think (M : Finset ℕ) (hM : M = (Finset.range n).filter (fun i => a i ∈ Set.Ioc 2 4)) is better than (M := (Finset.range n).filter (fun i => a i ∈ Set.Ioc 2 4)) which creates some optParam that's difficult to work with

[Lingwei Peng (彭灵伟)]

Thanks, I’ve updated it.

[Yaël Dillies]

Here is a simpler statement that directly implies yours:

theorem simpler_h_eq (M : Finset ℕ) :
    ∑ i ∈ M, #{l ∈ .range (i + 1) | l ∈ M} = ∑ i ∈ .range #M, (i + 1) := by
  sorry

[Yaël Dillies]

I suggest you first prove it when (M : Finset ℕ) is replaced by {M : List ℕ} (hM : M.Sorted (· < ·)), and do induction on M