-- 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₁ := 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