-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst_1 : CommRing A
φ : R →+* A
⊢ C.map φ • W.map φ = (C • W).map φ
have simp : {
    a₁ :=
      (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A) *
        HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₁ : A)
          (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.s : A)),
    a₂ :=
      HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A)
          2 *
        (HSub.hSub (α := A) ((φ : (a : R) → A) W.a₂ : A)
              (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.s : A) ((φ : (a : R) → A) W.a₁ : A)) +
            HMul.hMul (α := A) (β := A) (3 : A) ((φ : (a : R) → A) C.r : A) -
          HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.s : A) 2),
    a₃ :=
      HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A)
          3 *
        (HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₃ : A)
            (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) W.a₁ : A)) +
          HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.t : A)),
    a₄ :=
      HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A)
          4 *
        (HSub.hSub (α := A) ((φ : (a : R) → A) W.a₄ : A)
                  (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.s : A) ((φ : (a : R) → A) W.a₃ : A)) +
                HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.r : A))
                  ((φ : (a : R) → A) W.a₂ : A) -
              HMul.hMul (β := A)
                (HAdd.hAdd (α := A) ((φ : (a : R) → A) C.t : A)
                  (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C.s : A)))
                ((φ : (a : R) → A) W.a₁ : A) +
            3 * HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.r : A) 2 -
          HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.s : A))
            ((φ : (a : R) → A) C.t : A)),
    a₆ :=
      HPow.hPow (α := A) (β := ℕ) (↑(((Units.map (↑φ : R →* A) : MonoidHom.{u, v} Rˣ Aˣ) : (a : Rˣ) → Aˣ) C.u)⁻¹ : A)
          6 *
        (HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₆ : A)
                    (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) W.a₄ : A)) +
                  HMul.hMul (β := A) (HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.r : A) 2)
                    ((φ : (a : R) → A) W.a₂ : A) +
                HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.r : A) 3 -
              HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.t : A) ((φ : (a : R) → A) W.a₃ : A) -
            HPow.hPow (α := A) (β := ℕ) ((φ : (a : R) → A) C.t : A) 2 -
          HMul.hMul (β := A) (HMul.hMul (α := A) (β := A) ((φ : (a : R) → A) C.r : A) ((φ : (a : R) → A) C.t : A))
            ((φ : (a : R) → A) W.a₁ : A)) :
    WeierstrassCurve A } =
  { a₁ := (φ : (a : R) → A) ((↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s)),
    a₂ :=
      (φ : (a : R) → A) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2)),
    a₃ := (φ : (a : R) → A) (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)),
    a₄ :=
      (φ : (a : R) → A)
        (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)),
    a₆ :=
      (φ : (a : R) → A)
        (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₁)) }
Tactic: simp only [map, variableChange_def, VariableChange.map]