-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) (C.u * C'.u),
      r := (φ : (a : R) → A) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r),
      s := (φ : (a : R) → A) ((↑C'.u : R) * C.s + C'.s),
      t :=
        (φ : (a : R) → A)
          (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) } =
    {
      u :=
        HMul.hMul (α := Aˣ) (β := Aˣ) (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u : Aˣ)
          (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u : Aˣ),
      r :=
        HAdd.hAdd (β := A)
          (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
            (HPow.hPow (α := A) (β := ℕ)
              (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2))
          ((φ : (a : R) → A) C'.r : A),
      s :=
        HAdd.hAdd (β := A)
          (HMul.hMul (α := A) (β := A)
            ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
            ((φ : (a : R) → A) C.s : A))
          ((φ : (a : R) → A) C'.s : A),
      t :=
        HAdd.hAdd (β := A)
          (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
              (HPow.hPow (α := A) (β := ℕ)
                (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
            HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
              HPow.hPow (α := A) (β := ℕ)
                (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2)
          ((φ : (a : R) → A) C'.t : A) :
      VariableChange A }
have u : (↑(u
        { u := ((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) (C.u * C'.u),
          r := (φ : (a : R) → A) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r),
          s := (φ : (a : R) → A) ((↑C'.u : R) * C.s + C'.s),
          t :=
            (φ : (a : R) → A)
              (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) }) :
    A) =
  (↑{
          u :=
            HMul.hMul (α := Aˣ) (β := Aˣ)
              (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u : Aˣ)
              (((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u : Aˣ),
          r :=
            HAdd.hAdd (β := A)
              (HMul.hMul (α := A) ((φ : (a : R) → A) C.r : A)
                (HPow.hPow (α := A) (β := ℕ)
                  (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2))
              ((φ : (a : R) → A) C'.r : A),
          s :=
            HAdd.hAdd (β := A)
              (HMul.hMul (α := A) (β := A)
                ((↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) : A)
                ((φ : (a : R) → A) C.s : A))
              ((φ : (a : R) → A) C'.s : A),
          t :=
            HAdd.hAdd (β := A)
              (HMul.hMul (α := A) ((φ : (a : R) → A) C.t : A)
                  (HPow.hPow (α := A) (β := ℕ)
                    (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 3) +
                HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C'.s : A) *
                  HPow.hPow (α := A) (β := ℕ)
                    (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C'.u) : A) 2)
              ((φ : (a : R) → A) C'.t : A) :
          VariableChange A }.u :
    A)
Tactic: ext