-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
a₁ :
  { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₂ :=
          HPow.hPow (α := R) (β := ℕ) 1 2 *
            (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
                HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
        a₃ :=
          HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₄ :=
          HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                    HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                      W.a₂ -
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                      HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                    W.a₁ +
                3 *
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    2 -
              HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
        a₆ :=
          HPow.hPow (α := R) (β := ℕ) 1 6 *
            (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                      HPow.hPow (α := R) (β := ℕ)
                          (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 *
                        W.a₂ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      3 -
                  VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
                HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
              HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                W.a₁) :
        WeierstrassCurve R }.a₁ =
    W.a₁
a₂ :
  { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₂ :=
          HPow.hPow (α := R) (β := ℕ) 1 2 *
            (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
                HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
        a₃ :=
          HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₄ :=
          HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                    HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                      W.a₂ -
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                      HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                    W.a₁ +
                3 *
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    2 -
              HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
        a₆ :=
          HPow.hPow (α := R) (β := ℕ) 1 6 *
            (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                      HPow.hPow (α := R) (β := ℕ)
                          (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 *
                        W.a₂ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      3 -
                  VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
                HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
              HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                W.a₁) :
        WeierstrassCurve R }.a₂ =
    W.a₂
a₃ :
  { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₂ :=
          HPow.hPow (α := R) (β := ℕ) 1 2 *
            (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
                HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
        a₃ :=
          HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₄ :=
          HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                    HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                      W.a₂ -
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                      HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                    W.a₁ +
                3 *
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    2 -
              HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
        a₆ :=
          HPow.hPow (α := R) (β := ℕ) 1 6 *
            (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                      HPow.hPow (α := R) (β := ℕ)
                          (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 *
                        W.a₂ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      3 -
                  VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
                HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
              HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                W.a₁) :
        WeierstrassCurve R }.a₃ =
    W.a₃
⊢ { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
      a₂ :=
        HPow.hPow (α := R) (β := ℕ) 1 2 *
          (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
            HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
      a₃ :=
        HPow.hPow (α := R) (β := ℕ) 1 3 *
          (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
            HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
      a₄ :=
        HPow.hPow (α := R) (β := ℕ) 1 4 *
          (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                  HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) * W.a₂ -
                (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                    HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                  W.a₁ +
              3 *
                HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
            HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
              VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
      a₆ :=
        HPow.hPow (α := R) (β := ℕ) 1 6 *
          (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        2 *
                      W.a₂ +
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    3 -
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
            HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
              W.a₁) :
      WeierstrassCurve R } =
    W
have a₄ : { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
      a₂ :=
        HPow.hPow (α := R) (β := ℕ) 1 2 *
          (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
            HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
      a₃ :=
        HPow.hPow (α := R) (β := ℕ) 1 3 *
          (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
            HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
      a₄ :=
        HPow.hPow (α := R) (β := ℕ) 1 4 *
          (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                  HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) * W.a₂ -
                (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                    HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                  W.a₁ +
              3 *
                HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
            HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
              VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
      a₆ :=
        HPow.hPow (α := R) (β := ℕ) 1 6 *
          (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        2 *
                      W.a₂ +
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    3 -
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
            HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
              W.a₁) :
      WeierstrassCurve R }.a₄ =
  W.a₄
Tactic: ext