-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).Δ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 12 * W.Δ
have 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₆))
Tactic: simp only [b₂, b₄, b₆, b₈, Δ, variableChange_a₁, variableChange_a₂, variableChange_a₃,
    variableChange_a₄, variableChange_a₆]