Explicit summation for small sums

Stream: lean4

[Teddy Baker]

--- Meant to post this in "Is there code for X?"
I'd like an easy way to "unfold" a short sum. For Finset.Ico I found this way, which is not too bad, but I had trouble with using the repeat tactic on the rw

import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.BigOperators.Intervals
open BigOperators

lemma sum_lem : ∑ n in Finset.Ico 3 (3 + 4), g n = g 3 + g 4 + g 5 + g 6 := by
    rw [Finset.sum_eq_sum_Ico_succ_bot]
    rw [Finset.sum_eq_sum_Ico_succ_bot]
    rw [Finset.sum_eq_sum_Ico_succ_bot]
    rw [Finset.sum_eq_sum_Ico_succ_bot]
    -- Extra simplification before closing goal

Just wondering if this is the simplest way. I tried using the repeat tactic and that went into an infinite loop and crashed the lean server.

[James Gallicchio]

does simp [Finset.sum_eq_sum_Ico_succ_bot] do the right thing? I'm sorta surprised if it doesn't

[Teddy Baker]

James Gallicchio said:

does simp [Finset.sum_eq_sum_Ico_succ_bot] do the right thing? I'm sorta surprised if it doesn't

Yes that's better, thanks!

[James Gallicchio]

simp [x] does use an entirely different algorithm from rw [x], so it can't always be dropped in for rw, but for most common cases simp is like a repeated rewrite :D