Proving an equality with supremum of an indexed family

Stream: new members

[Vlad]

While the equation below appears straightforward, I'm wondering if there's a relevant lemma that could be helpful in proving it. I found lemmas about supremum of an (bounded) indexed family in the Real, Language, and Cardinality packages, but I haven't been able to connect them directly to this problem.

import Lean
import Mathlib.Tactic
open Lean Finset Algebra

example {i : ℕ} {xs: Array ℤ}
  (h0: 0 < i)
  (hi: i < xs.size)
  := calc xs[i] + (⨆ a ∈ range i, xs[a]'sorry)
        _ = ⨆ a ∈ range i, (xs[i] + xs[a]'sorry)   := sorry -- by rw [add_ciSup]