-- 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
⊢ {
        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₁
      { 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₁)) }
have 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)) =
  HMul.hMul (α := A) ((φ : (a : R) → A) (↑C.u⁻¹ : R) : A)
    (HAdd.hAdd (α := A) ((φ : (a : R) → A) W.a₁ : A) (HMul.hMul (α := A) (β := A) (2 : A) ((φ : (a : R) → A) C.s : A)))
Tactic: map_simp