Rewrite summation without simp_rw

Stream: new members

[Karthik 🦋]

Hi, I'm working through a telescoping sum problem in lean and I'm not allowed to use simp, ring, linarith etc.
How do I rewrite the expression inside the sum without simp_rw?

theorem induction_sum_1oktkp1
  (n : ℕ) :
  ∑ k in (Finset.range n), (1 : ℝ) / ((k + 1) * (k + 2)) = n / (n + 1) := by

  have is_tele (k : ℕ) : (1 : ℝ) / ((k + 1) * (k + 2)) = (1 : ℝ) / (k + 1) - (1 : ℝ) / (k + 2) := by
    rw [div_sub_div]
    case hb => norm_cast
    case hd => norm_cast
    rw [one_mul, mul_one, add_comm _ 2, add_sub_assoc, sub_add_eq_sub_sub, sub_self, zero_sub]
    norm_num1
    rfl

  rw [is_tele] --does not work
  -- simp_rw [is_tele]; --works

Additionally, since norm_cast uses simp, I'd like to avoid that, I want to prove ↑k + 1 ≠ 0 where k : ℕ is being upcast to a real. The closest thing I have right now is Real.toNNReal_eq_nat_cast.

[Edward van de Meent]

something like Finset.sum_congr might help?

[Etienne Marion]

import Mathlib

theorem induction_sum_1oktkp1
  (n : ℕ) :
  ∑ k in (Finset.range n), (1 : ℝ) / ((k + 1) * (k + 2)) = n / (n + 1) := by

  have is_tele (k : ℕ) : (1 : ℝ) / ((k + 1) * (k + 2)) = (1 : ℝ) / (k + 1) - (1 : ℝ) / (k + 2) := by
    rw [div_sub_div]
    case hb => norm_cast
    case hd => norm_cast
    rw [one_mul, mul_one, add_comm _ 2, add_sub_assoc, sub_add_eq_sub_sub, sub_self, zero_sub]
    norm_num1
    rfl

  have (k : ℕ) : (k + 1 : ℝ) ≠ 0 := Nat.cast_add_one_ne_zero k

  rw [Finset.sum_congr rfl (fun _ _ ↦ is_tele _)]

[Karthik 🦋]

Thank you.
I was stuck looking at casting lemmas in the Real namespace :sweat_smile: