-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
simp :
  -HPow.hPow (β := ℕ)
                (HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s)) 2 +
                  4 * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2)))
                2 *
            (HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s)) 2 *
                      (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₁)) +
                    4 * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2)) *
                      (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.u⁻¹ : R) * (W.a₁ + 2 * C.s) *
                      (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) *
                    (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.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2) *
                  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) 2 -
              HPow.hPow (β := ℕ)
                (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))
                2) -
          8 *
            HPow.hPow (β := ℕ)
              (2 *
                  (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.u⁻¹ : R) * (W.a₁ + 2 * C.s) * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)))
              3 -
        27 *
          HPow.hPow (β := ℕ)
            (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) 2 +
              4 *
                (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₁)))
            2 +
      9 *
            (HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s)) 2 +
              4 * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2))) *
          (2 *
              (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.u⁻¹ : R) * (W.a₁ + 2 * C.s) * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t))) *
        (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) 2 +
          4 *
            (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₁))) =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 *
      (-HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) 2 *
              (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ +
                  W.a₂ * HPow.hPow (β := ℕ) W.a₃ 2 -
                HPow.hPow (β := ℕ) W.a₄ 2) -
            8 * HPow.hPow (β := ℕ) (2 * W.a₄ + W.a₁ * W.a₃) 3 -
          27 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆) 2 +
        9 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (HPow.hPow (β := ℕ) W.a₃ 2 + 4 * W.a₆))
⊢ (C • W).Δ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ

Tactic:
simp only [b₂, b₄, b₆, b₈, Δ, variableChange_a₁, variableChange_a₂, variableChange_a₃,
    variableChange_a₄, variableChange_a₆]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.variableChange_a₁, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.variableChange_a₂, WeierstrassCurve.variableChange_a₃, WeierstrassCurve.b₈, WeierstrassCurve.variableChange_a₄, WeierstrassCurve.variableChange_a₆, WeierstrassCurve.b₆