Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ { a₁ := 1 * (W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.s),
      a₂ :=
        1 ^ 2 *
          (W.a₂ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₁ + 3 * { u := 1, r := 0, s := 0, t := 0 }.r -
            { u := 1, r := 0, s := 0, t := 0 }.s ^ 2),
      a₃ := 1 ^ 3 * (W.a₃ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.t),
      a₄ :=
        1 ^ 4 *
          (W.a₄ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₃ + 2 * { u := 1, r := 0, s := 0, t := 0 }.r * W.a₂ -
                ({ u := 1, r := 0, s := 0, t := 0 }.t +
                    { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.s) *
                  W.a₁ +
              3 * { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 -
            2 * { u := 1, r := 0, s := 0, t := 0 }.s * { u := 1, r := 0, s := 0, t := 0 }.t),
      a₆ :=
        1 ^ 6 *
          (W.a₆ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₄ + { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 * W.a₂ +
                  { u := 1, r := 0, s := 0, t := 0 }.r ^ 3 -
                { u := 1, r := 0, s := 0, t := 0 }.t * W.a₃ -
              { u := 1, r := 0, s := 0, t := 0 }.t ^ 2 -
            { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.t * W.a₁) } =
    W

Tactic:
ext

Goal state after:
case a₁
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ { a₁ := 1 * (W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.s),
        a₂ :=
          1 ^ 2 *
            (W.a₂ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₁ + 3 * { u := 1, r := 0, s := 0, t := 0 }.r -
              { u := 1, r := 0, s := 0, t := 0 }.s ^ 2),
        a₃ := 1 ^ 3 * (W.a₃ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₁ + 2 * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₄ :=
          1 ^ 4 *
            (W.a₄ - { u := 1, r := 0, s := 0, t := 0 }.s * W.a₃ + 2 * { u := 1, r := 0, s := 0, t := 0 }.r * W.a₂ -
                  ({ u := 1, r := 0, s := 0, t := 0 }.t +
                      { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.s) *
                    W.a₁ +
                3 * { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 -
              2 * { u := 1, r := 0, s := 0, t := 0 }.s * { u := 1, r := 0, s := 0, t := 0 }.t),
        a₆ :=
          1 ^ 6 *
            (W.a₆ + { u := 1, r := 0, s := 0, t := 0 }.r * W.a₄ + { u := 1, r := 0, s := 0, t := 0 }.r ^ 2 * W.a₂ +
                    { u := 1, r := 0, s := 0, t := 0 }.r ^ 3 -
                  { u := 1, r := 0, s := 0, t := 0 }.t * W.a₃ -
                { u := 1, r := 0, s := 0, t := 0 }.t ^ 2 -
              { u := 1, r := 0, s := 0, t := 0 }.r * { u := 1, r := 0, s := 0, t := 0 }.t * W.a₁) }.a₁ =
    W.a₁

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

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

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

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