Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: 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₁

pp: 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₂

pp: 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₃

pp: 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₄

pp: 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₆

Tactic:
<;>

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₆