-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma variableChange_id : W.variableChange VariableChange.id = W

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.variableChange VariableChange.id = W

Tactic:
rw [VariableChange.id, variableChange, inv_one, Units.val_one]

Result:
R : Type u
inst✝ : CommRing 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

Proof state:
case a₆
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 1 ^ 6 * (W.a₆ + 0 * W.a₄ + 0 ^ 2 * W.a₂ + 0 ^ 3 - 0 * W.a₃ - 0 ^ 2 - 0 * 0 * W.a₁) = W.a₆

Tactic:
ring1

Result:
no goals

Proof state:
case a₆
R : Type u
inst✝ : CommRing 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:
dsimp only

Result:
case a₆
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 1 ^ 6 * (W.a₆ + 0 * W.a₄ + 0 ^ 2 * W.a₂ + 0 ^ 3 - 0 * W.a₃ - 0 ^ 2 - 0 * 0 * W.a₁) = W.a₆

Proof state:
R : Type u
inst✝ : CommRing 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 <;> (dsimp only; ring1)

Result:
no goals