Algebraic manipulations with fractions and lean3 to lean4

Stream: new members

[Nowhere Dense]

I'm still learning basic lean and I'm struggling now with some basic algebraic manipulations.
I want to prove the following:

example {r : ℝ} (n : ℕ) (h : r ≠ 1) :
  (r^(n+1) - 1) / (r-1) + r ^ (n+1) =(r^(n+1+1) - 1) / (r-1) := by sorry

But I can't figure out the right tactics to do it. I found the following example on the mathlib3 documentation

example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
  a + b / x + c / x^2 + d / x^3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) :=
begin
  field_simp,
  ring
end

I'm pretty sure this could help in my case but the syntax is in lean 3, any idea of how to translate the begin ... end syntax to lean 4?

[Ilmārs Cīrulis]

This worked for me:

import Mathlib

example {r : ℝ} (n : ℕ) (h : r ≠ 1) :
    (r ^ (n + 1) - 1) / (r - 1) + r ^ (n + 1) = (r ^ (n + 1 + 1) - 1) / (r - 1) := by
  have H: r - 1 ≠ 0 := sub_ne_zero_of_ne h
  field_simp
  ring

[Nowhere Dense]

Thank you! it works for me too