-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma variableChange_comp (C C' : VariableChange R) (W : WeierstrassCurve R) :
    W.variableChange (C.comp C') = (W.variableChange C').variableChange C

Proof state:
R : Type u
inst✝ : CommRing R
C C' : VariableChange R
W : WeierstrassCurve R
⊢ W.variableChange (C.comp C') = (W.variableChange C').variableChange C

Tactic:
simp only [VariableChange.comp, variableChange]

Result:
R : Type u
inst✝ : CommRing R
C C' : VariableChange R
W : WeierstrassCurve R
⊢ { a₁ := ↑(C.u * C'.u)⁻¹ * (W.a₁ + 2 * (↑C'.u * C.s + C'.s)),
      a₂ :=
        ↑(C.u * C'.u)⁻¹ ^ 2 *
          (W.a₂ - (↑C'.u * C.s + C'.s) * W.a₁ + 3 * (C.r * ↑C'.u ^ 2 + C'.r) - (↑C'.u * C.s + C'.s) ^ 2),
      a₃ :=
        ↑(C.u * C'.u)⁻¹ ^ 3 *
          (W.a₃ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₁ + 2 * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)),
      a₄ :=
        ↑(C.u * C'.u)⁻¹ ^ 4 *
          (W.a₄ - (↑C'.u * C.s + C'.s) * W.a₃ + 2 * (C.r * ↑C'.u ^ 2 + C'.r) * W.a₂ -
                (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t + (C.r * ↑C'.u ^ 2 + C'.r) * (↑C'.u * C.s + C'.s)) *
                  W.a₁ +
              3 * (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 -
            2 * (↑C'.u * C.s + C'.s) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)),
      a₆ :=
        ↑(C.u * C'.u)⁻¹ ^ 6 *
          (W.a₆ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₄ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 * W.a₂ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 3 -
                (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₃ -
              (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) ^ 2 -
            (C.r * ↑C'.u ^ 2 + C'.r) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₁) } =
    { a₁ := ↑C.u⁻¹ * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s) + 2 * C.s),
      a₂ :=
        ↑C.u⁻¹ ^ 2 *
          (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2) - C.s * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 3 * C.r -
            C.s ^ 2),
      a₃ :=
        ↑C.u⁻¹ ^ 3 * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t) + C.r * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 2 * C.t),
      a₄ :=
        ↑C.u⁻¹ ^ 4 *
          (↑C'.u⁻¹ ^ 4 *
                      (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 -
                        2 * C'.s * C'.t) -
                    C.s * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) +
                  2 * C.r * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) -
                (C.t + C.r * C.s) * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) +
              3 * C.r ^ 2 -
            2 * C.s * C.t),
      a₆ :=
        ↑C.u⁻¹ ^ 6 *
          (↑C'.u⁻¹ ^ 6 *
                        (W.a₆ + C'.r * W.a₄ + C'.r ^ 2 * W.a₂ + C'.r ^ 3 - C'.t * W.a₃ - C'.t ^ 2 -
                          C'.r * C'.t * W.a₁) +
                      C.r *
                        (↑C'.u⁻¹ ^ 4 *
                          (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 -
                            2 * C'.s * C'.t)) +
                    C.r ^ 2 * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) +
                  C.r ^ 3 -
                C.t * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) -
              C.t ^ 2 -
            C.r * C.t * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s))) }