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