Rewriting inside a function

Stream: new members

[Stepan Nesterov]

Is this a good way to rw inside a function?

/-- If `a(n)` tends to `t` and `b(n)` tends to `u` then
`a(n)*b(n)` tends to `t*u`. -/
theorem tendsTo_mul (a b : ℕ → ℝ) (t u : ℝ) (ha : TendsTo a t) (hb : TendsTo b u) :
    TendsTo (fun n ↦ a n * b n) (t * u) := by
  rw [show (fun n ↦ a n * b n) = (fun n ↦ (a n - t) * (b n - u)) + (fun n ↦ t * b n) + (fun n ↦ u * a n) - (fun n ↦ t * u)
    by ext n; dsimp; ring]
  rw [show t * u = 0 + t * u + u * t - t * u by ring]

I'm using an exercise from https://github.com/ImperialCollegeLondon/formalising-mathematics-2024, section 2, sheet 6 as an example

[Aaron Liu]

you can use conv-mode

[Kevin Buzzard]

or maybe simp_rw?