Finset.sum_Icc_one_eq_sum_range

theorem _root_.Finset.sum_Icc_one_eq_sum_range {N : ℕ} (f : ℕ → 𝕜) :    ∑ k ∈ Icc 1 N, f k = ∑ n ∈ range N, f (n + 1) := by  symm  refine sum_bij (s := range N) (t := Icc 1 N)    (f := fun n => f (n + 1)) (g := fun k => f k)    (i := fun n _ => n + 1)    ?hi ?hinj ?hsurj ?hcongr  · intro n hn    have hlt : n < N := mem_range.mp hn    exact mem_Icc.mpr ⟨Nat.succ_le_succ (Nat.zero_le n), Nat.succ_le_of_lt hlt⟩  · intro a ha b hb h    exact Nat.succ_injective h  · intro k hk    rcases mem_Icc.mp hk with ⟨hk1, hk2⟩    refine ⟨k - 1, mem_range.mpr ?_, ?_⟩    · have hsucc : (k - 1) + 1 = k := Nat.sub_add_cancel hk1      exact lt_of_lt_of_le (Nat.lt_succ_self _) (by simpa [hsucc] using hk2)    · simp [Nat.sub_add_cancel hk1]  · intro n hn    rfl