Finset.Icc error

Stream: new members

[Janitha]

Finset.Icc 1 97

gives me an error: failed to synthesize
Preorder ℂ

I want to write

(∑ k ∈ Finset.Icc 1 97, k * (Complex.I ^ k)) = 48 + 49 * Complex.I

Context ---> I'm trying to formalize a proof of:

example (n : ℕ) : (∑ k ∈ Finset.Icc 1 n, k * (Complex.I ^ k)) = 48 + 49 * Complex.I ↔ n = 97 := by sorry

[Yaël Dillies]

What if you do k ∈ Finset.Icc (1 : ℕ) 97?

[Janitha]

That worked. Thanks!

[Tiru Arthanari]

Hi, I am new to coding in Lean4. How do I fix the issue with:

import Mathlib
def increasingTriples (n : ℕ) : Finset (ℕ × ℕ × ℕ) :=

  (Finset.Icc 1 n).filterMap (λ i =>

    (Finset.Icc (i + 1) n).filterMap (λ j =>

      (Finset.Icc (j + 1) n).map (λ k => (i, j, k))

    )

  ) (by simp)

[Snir Broshi]

import Mathlib
def increasingTriples (n : ℕ) : Finset (ℕ × ℕ × ℕ) :=
  (Finset.Icc 1 n).biUnion fun i ↦
    (Finset.Icc (i + 1) n).biUnion fun j ↦
      (Finset.Icc (j + 1) n).image fun k ↦ (i, j, k)

You can also start with all triples and filter only the increasing ones.

[Snir Broshi]

You can use #eval increasingTriples 5 to see if this is the result you expected