-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
u :
  (↑{
            u :=
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
                C.u,
            r :=
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                      t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                  HPow.hPow (β := ℕ) (↑C.u : R) 2 +
                C.r,
            s :=
              (↑C.u : R) *
                  { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                      t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
                C.s,
            t :=
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                        t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
                    HPow.hPow (β := ℕ) (↑C.u : R) 3 +
                  { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                          t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                      C.s *
                    HPow.hPow (β := ℕ) (↑C.u : R) 2 +
                C.t :
            VariableChange R }.u :
      R) =
    (↑(VariableChange.u { u := 1, r := 0, s := 0, t := 0 }) : R)
r :
  {
        u :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
            C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
              HPow.hPow (β := ℕ) (↑C.u : R) 2 +
            C.r,
        s :=
          (↑C.u : R) *
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
                HPow.hPow (β := ℕ) (↑C.u : R) 3 +
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                      t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                  C.s *
                HPow.hPow (β := ℕ) (↑C.u : R) 2 +
            C.t :
        VariableChange R }.r =
    VariableChange.r { u := 1, r := 0, s := 0, t := 0 }
⊢ {
      u :=
        { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
              t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
          C.u,
      r :=
        { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
            HPow.hPow (β := ℕ) (↑C.u : R) 2 +
          C.r,
      s :=
        (↑C.u : R) *
            { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
          C.s,
      t :=
        { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
              HPow.hPow (β := ℕ) (↑C.u : R) 3 +
            { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                C.s *
              HPow.hPow (β := ℕ) (↑C.u : R) 2 +
          C.t :
      VariableChange R } =
    { u := 1, r := 0, s := 0, t := 0 }
have s : {
      u :=
        { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
              t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
          C.u,
      r :=
        { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
            HPow.hPow (β := ℕ) (↑C.u : R) 2 +
          C.r,
      s :=
        (↑C.u : R) *
            { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
          C.s,
      t :=
        { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
              HPow.hPow (β := ℕ) (↑C.u : R) 3 +
            { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                C.s *
              HPow.hPow (β := ℕ) (↑C.u : R) 2 +
          C.t :
      VariableChange R }.s =
  s { u := 1, r := 0, s := 0, t := 0 }
Tactic: ext