-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C_1 C C' : VariableChange R
W : WeierstrassCurve R
⊢ { a₁ := (↑(C.u * C'.u)⁻¹ : R) * (W.a₁ + 2 * ((↑C'.u : R) * C.s + C'.s)),
      a₂ :=
        HPow.hPow (β := ℕ) (↑(C.u * C'.u)⁻¹ : R) 2 *
          (W.a₂ - ((↑C'.u : R) * C.s + C'.s) * W.a₁ + 3 * (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) -
            HPow.hPow (β := ℕ) ((↑C'.u : R) * C.s + C'.s) 2),
      a₃ :=
        HPow.hPow (β := ℕ) (↑(C.u * C'.u)⁻¹ : R) 3 *
          (W.a₃ + (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * W.a₁ +
            2 * (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t)),
      a₄ :=
        HPow.hPow (β := ℕ) (↑(C.u * C'.u)⁻¹ : R) 4 *
          (W.a₄ - ((↑C'.u : R) * C.s + C'.s) * W.a₃ + 2 * (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * W.a₂ -
                (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t +
                    (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * ((↑C'.u : R) * C.s + C'.s)) *
                  W.a₁ +
              3 * HPow.hPow (β := ℕ) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) 2 -
            2 * ((↑C'.u : R) * C.s + C'.s) *
              (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t)),
      a₆ :=
        HPow.hPow (β := ℕ) (↑(C.u * C'.u)⁻¹ : R) 6 *
          (W.a₆ + (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * W.a₄ +
                    HPow.hPow (β := ℕ) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) 2 * W.a₂ +
                  HPow.hPow (β := ℕ) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) 3 -
                (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) * W.a₃ -
              HPow.hPow (β := ℕ)
                (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) 2 -
            (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) *
                (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) *
              W.a₁) :
      WeierstrassCurve R } =
    { a₁ := (↑C.u⁻¹ : R) * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s) + 2 * C.s),
      a₂ :=
        HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 *
          (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - HPow.hPow (β := ℕ) C'.s 2) -
                C.s * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s)) +
              3 * C.r -
            HPow.hPow (β := ℕ) C.s 2),
      a₃ :=
        HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 *
          (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t) +
              C.r * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s)) +
            2 * C.t),
      a₄ :=
        HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 *
          (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) -
                    C.s * (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) +
                  2 * C.r *
                    (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - HPow.hPow (β := ℕ) C'.s 2)) -
                (C.t + C.r * C.s) * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s)) +
              3 * HPow.hPow (β := ℕ) C.r 2 -
            2 * C.s * C.t),
      a₆ :=
        HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 *
          (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₁) +
                      C.r *
                        (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)) +
                    HPow.hPow (β := ℕ) C.r 2 *
                      (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 2 *
                        (W.a₂ - C'.s * W.a₁ + 3 * C'.r - HPow.hPow (β := ℕ) C'.s 2)) +
                  HPow.hPow (β := ℕ) C.r 3 -
                C.t * (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) -
              HPow.hPow (β := ℕ) C.t 2 -
            C.r * C.t * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s))) }
have a₁ : { a₁ := (↑(C.u * C'.u)⁻¹ : R) * (W.a₁ + 2 * ((↑C'.u : R) * C.s + C'.s)),
      a₂ :=
        HPow.hPow (β := ℕ) (↑(C.u * C'.u)⁻¹ : R) 2 *
          (W.a₂ - ((↑C'.u : R) * C.s + C'.s) * W.a₁ + 3 * (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) -
            HPow.hPow (β := ℕ) ((↑C'.u : R) * C.s + C'.s) 2),
      a₃ :=
        HPow.hPow (β := ℕ) (↑(C.u * C'.u)⁻¹ : R) 3 *
          (W.a₃ + (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * W.a₁ +
            2 * (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t)),
      a₄ :=
        HPow.hPow (β := ℕ) (↑(C.u * C'.u)⁻¹ : R) 4 *
          (W.a₄ - ((↑C'.u : R) * C.s + C'.s) * W.a₃ + 2 * (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * W.a₂ -
                (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t +
                    (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * ((↑C'.u : R) * C.s + C'.s)) *
                  W.a₁ +
              3 * HPow.hPow (β := ℕ) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) 2 -
            2 * ((↑C'.u : R) * C.s + C'.s) *
              (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t)),
      a₆ :=
        HPow.hPow (β := ℕ) (↑(C.u * C'.u)⁻¹ : R) 6 *
          (W.a₆ + (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * W.a₄ +
                    HPow.hPow (β := ℕ) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) 2 * W.a₂ +
                  HPow.hPow (β := ℕ) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) 3 -
                (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) * W.a₃ -
              HPow.hPow (β := ℕ)
                (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) 2 -
            (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) *
                (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) *
              W.a₁) :
      WeierstrassCurve R }.a₁ =
  { a₁ := (↑C.u⁻¹ : R) * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s) + 2 * C.s),
      a₂ :=
        HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 *
          (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - HPow.hPow (β := ℕ) C'.s 2) -
                C.s * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s)) +
              3 * C.r -
            HPow.hPow (β := ℕ) C.s 2),
      a₃ :=
        HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 *
          (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t) +
              C.r * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s)) +
            2 * C.t),
      a₄ :=
        HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 *
          (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) -
                    C.s * (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) +
                  2 * C.r *
                    (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - HPow.hPow (β := ℕ) C'.s 2)) -
                (C.t + C.r * C.s) * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s)) +
              3 * HPow.hPow (β := ℕ) C.r 2 -
            2 * C.s * C.t),
      a₆ :=
        HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 *
          (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₁) +
                      C.r *
                        (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)) +
                    HPow.hPow (β := ℕ) C.r 2 *
                      (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 2 *
                        (W.a₂ - C'.s * W.a₁ + 3 * C'.r - HPow.hPow (β := ℕ) C'.s 2)) +
                  HPow.hPow (β := ℕ) C.r 3 -
                C.t * (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) -
              HPow.hPow (β := ℕ) C.t 2 -
            C.r * C.t * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s))) }.a₁
Tactic: ext