Sum on a subtype: I am getting this wrong

Stream: new members

[Philippe Duchon]

I am trying to state and prove a theorem that involves infinite sums and sums over a subtype, but somehow I cannot even state it - Lean tells me there is a type mismatch, and I don't understand what it is.

import Mathlib

section Sums

variable {T: Type}
variable {K: Type} [Ring K] [TopologicalSpace K] [UniformSpace K] [IsTopologicalRing K]
variable [CompleteSpace K] [T2Space K]

variable (Φ: T ≃ T) (w: T → K)

variable (hf: ∀ x, Φ x = x ∨ w (Φ x) = - w x)

variable (hsum: Summable w)

theorem sum_fixedpoints: Σ' (x : T), w x = Σ' (x : ↑ {y | Φ y = y }), w (↑x) := by sorry

end Sums

Lean tells me that w ↑x has type T (which is what I expected), but it is expecting something different (Sort ?u.3495 : Type ?u.3495), and I don't understand why this is.

I have tried with and without the ↑, Lean correctly inserts the coercions, so it does not seem to be the source of the problem.

[Marcus Rossel]

I think parentheses might be necessary here. Your current statement groups as follows:

Σ' (x : T), (w x = Σ' (x : ↑ {y | Φ y = y }), w (↑x))

[Riccardo Brasca]

Also, you are using \Sigma instead of \sum

[Riccardo Brasca]

theorem sum_fixedpoints: ∑' (x : T), w x = ∑' (x : {y | Φ y = y }), w x := by
  sorry

this works (Lean automatically inserts coercions for you)

[Philippe Duchon]

Riccardo Brasca said:

Also, you are using \Sigma instead of \sum

And it's not even the first time I do this (with \sum, no additional parentheses are necessary)

Thanks! (I will probably make the same mistake again, but hopefully I'll check before coming back)

Is there a simple way, from within Lean, to check for what a notation is about?

[Riccardo Brasca]

I noticed it because I use \sum much more than \Sigma, and the symbol looked strange to me. Anyway if you hoover with the cursors you get some information, and on \Sigma there is nothing about sums.

[Philippe Duchon]

Yeah, but with \Sigma there is no additional information, so it's only a hint if you really expect to get some.

Also, I think \Sigma looks nicer than \sum, so I don't initially notice the problem :)

[Riccardo Brasca]

The fact that the docstring doesn't mention sums it's what should make you suspicious (of course sometimes we are just missing documentation...)