-- 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 :
  (↑(VariableChange.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)
r :
  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 }.r
s :
  VariableChange.s
      { 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 }.s
⊢ { 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 t : t
    { 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 }.t
Tactic: ext