Need help with element from range having wrong type

Stream: new members

[Kevin Cheung]

I am trying to do the following:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Finset.Basic

open Finset

example (n : ℕ) (a : range n → ℝ) : ∀ i ∈ range n, a i ≤ abs (a i) := by sorry

Lean is complaining that i has incorrect type:

application type mismatch
  a i
argument
  i
has type
  ℕ : Type
but is expected to have type
  { x // x ∈ range n } : TypeLean 4
i : ℕ

To fix it, I could do:

example (n : ℕ) (a : ℕ → ℝ) : ∀ i ∈ range n, a i ≤ abs (a i) := by sorry

But is there a way to make the original version work?

[Ruben Van de Velde]

If you're going to coerce range n to a type anyway, you might use ∀ i : range n

[Kevin Cheung]

It works. Thanks. But I am a bit confused about the difference. So how does i ∈ range n differ from i : range n?

[Ruben Van de Velde]

One is i : Nat with a separate membership hypothesis, the other has the membership bundled up in a Subtype

[Kevin Cheung]

Does that mean that in ∑ i in range 4, h i, the index i will be a Nat and the property that i satisfies (i.e. 0 <= i < 4) is inaccessible?

[Ruben Van de Velde]

In that context, yes. You can use Finset.attach

[Yaël Dillies]

I am working to make ∑ hi : i ∈ range 4, h i notation be the version you want