awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
rw :
  { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
      a₂ :=
        HPow.hPow (α := R) (β := ℕ) 1 2 *
          (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
            HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
      a₃ :=
        HPow.hPow (α := R) (β := ℕ) 1 3 *
          (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
            HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
      a₄ :=
        HPow.hPow (α := R) (β := ℕ) 1 4 *
          (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                  HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) * W.a₂ -
                (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                    HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                  W.a₁ +
              3 *
                HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
            HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
              VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
      a₆ :=
        HPow.hPow (α := R) (β := ℕ) 1 6 *
          (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        2 *
                      W.a₂ +
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    3 -
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
            HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
              W.a₁) :
      WeierstrassCurve R } =
    W
⊢ HSMul.hSMul (α := VariableChange R) 1 W = W

Tactic:
rw [VariableChange.one_def, variableChange_def, inv_one, Units.val_one]

Premises used: inv_one, WeierstrassCurve.variableChange_def, WeierstrassCurve.VariableChange.one_def, Units.val_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
a₁ : 1 * (W.a₁ + HMul.hMul (α := R) 2 0) = W.a₁
⊢ { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₂ :=
          HPow.hPow (α := R) (β := ℕ) 1 2 *
            (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
                HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
        a₃ :=
          HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₄ :=
          HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                    HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                      W.a₂ -
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                      HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                    W.a₁ +
                3 *
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    2 -
              HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
        a₆ :=
          HPow.hPow (α := R) (β := ℕ) 1 6 *
            (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                      HPow.hPow (α := R) (β := ℕ)
                          (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 *
                        W.a₂ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      3 -
                  VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
                HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
              HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                W.a₁) :
        WeierstrassCurve R }.a₁ =
    W.a₁

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
a₂ :
  HPow.hPow (α := R) (β := ℕ) 1 2 * (W.a₂ - 0 * W.a₁ + HMul.hMul (α := R) 3 0 - HPow.hPow (α := R) (β := ℕ) 0 2) = W.a₂
⊢ { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₂ :=
          HPow.hPow (α := R) (β := ℕ) 1 2 *
            (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
                HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
        a₃ :=
          HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₄ :=
          HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                    HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                      W.a₂ -
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                      HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                    W.a₁ +
                3 *
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    2 -
              HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
        a₆ :=
          HPow.hPow (α := R) (β := ℕ) 1 6 *
            (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                      HPow.hPow (α := R) (β := ℕ)
                          (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 *
                        W.a₂ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      3 -
                  VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
                HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
              HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                W.a₁) :
        WeierstrassCurve R }.a₂ =
    W.a₂

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
a₃ : HPow.hPow (α := R) (β := ℕ) 1 3 * (W.a₃ + 0 * W.a₁ + HMul.hMul (α := R) 2 0) = W.a₃
⊢ { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₂ :=
          HPow.hPow (α := R) (β := ℕ) 1 2 *
            (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
                HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
        a₃ :=
          HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₄ :=
          HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                    HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                      W.a₂ -
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                      HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                    W.a₁ +
                3 *
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    2 -
              HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
        a₆ :=
          HPow.hPow (α := R) (β := ℕ) 1 6 *
            (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                      HPow.hPow (α := R) (β := ℕ)
                          (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 *
                        W.a₂ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      3 -
                  VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
                HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
              HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                W.a₁) :
        WeierstrassCurve R }.a₃ =
    W.a₃

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
a₄ :
  HPow.hPow (α := R) (β := ℕ) 1 4 *
      (W.a₄ - 0 * W.a₃ + HMul.hMul (α := R) 2 0 * W.a₂ - (0 + HMul.hMul (α := R) 0 0) * W.a₁ +
          3 * HPow.hPow (α := R) (β := ℕ) 0 2 -
        HMul.hMul (α := R) 2 0 * 0) =
    W.a₄
⊢ { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₂ :=
          HPow.hPow (α := R) (β := ℕ) 1 2 *
            (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
                HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
        a₃ :=
          HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₄ :=
          HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                    HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                      W.a₂ -
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                      HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                    W.a₁ +
                3 *
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    2 -
              HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
        a₆ :=
          HPow.hPow (α := R) (β := ℕ) 1 6 *
            (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                      HPow.hPow (α := R) (β := ℕ)
                          (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 *
                        W.a₂ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      3 -
                  VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
                HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
              HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                W.a₁) :
        WeierstrassCurve R }.a₄ =
    W.a₄

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
a₆ :
  HPow.hPow (α := R) (β := ℕ) 1 6 *
      (W.a₆ + 0 * W.a₄ + HPow.hPow (α := R) (β := ℕ) 0 2 * W.a₂ + HPow.hPow (α := R) (β := ℕ) 0 3 - 0 * W.a₃ -
          HPow.hPow (α := R) (β := ℕ) 0 2 -
        HMul.hMul (α := R) 0 0 * W.a₁) =
    W.a₆
⊢ { a₁ := 1 * (W.a₁ + HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₂ :=
          HPow.hPow (α := R) (β := ℕ) 1 2 *
            (W.a₂ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
                HMul.hMul (α := R) 3 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) -
              HPow.hPow (α := R) (β := ℕ) (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2),
        a₃ :=
          HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₁ +
              HMul.hMul (α := R) 2 (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R })),
        a₄ :=
          HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ +
                    HMul.hMul (α := R) 2 (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                      W.a₂ -
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } +
                      HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                        (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R })) *
                    W.a₁ +
                3 *
                  HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                    2 -
              HMul.hMul (α := R) 2 (VariableChange.s { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }),
        a₆ :=
          HPow.hPow (α := R) (β := ℕ) 1 6 *
            (W.a₆ + VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₄ +
                      HPow.hPow (α := R) (β := ℕ)
                          (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 *
                        W.a₂ +
                    HPow.hPow (α := R) (β := ℕ) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                      3 -
                  VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R } * W.a₃ -
                HPow.hPow (α := R) (β := ℕ) (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) 2 -
              HMul.hMul (α := R) (VariableChange.r { u := 1, r := 0, s := 0, t := 0 : VariableChange R })
                  (VariableChange.t { u := 1, r := 0, s := 0, t := 0 : VariableChange R }) *
                W.a₁) :
        WeierstrassCurve R }.a₆ =
    W.a₆

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 * (W.a₁ + HMul.hMul (α := R) 2 0) = W.a₁

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ HPow.hPow (α := R) (β := ℕ) 1 2 * (W.a₂ - 0 * W.a₁ + HMul.hMul (α := R) 3 0 - HPow.hPow (α := R) (β := ℕ) 0 2) = W.a₂

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ HPow.hPow (α := R) (β := ℕ) 1 3 * (W.a₃ + 0 * W.a₁ + HMul.hMul (α := R) 2 0) = W.a₃

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ HPow.hPow (α := R) (β := ℕ) 1 4 *
      (W.a₄ - 0 * W.a₃ + HMul.hMul (α := R) 2 0 * W.a₂ - (0 + HMul.hMul (α := R) 0 0) * W.a₁ +
          3 * HPow.hPow (α := R) (β := ℕ) 0 2 -
        HMul.hMul (α := R) 2 0 * 0) =
    W.a₄

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ HPow.hPow (α := R) (β := ℕ) 1 6 *
      (W.a₆ + 0 * W.a₄ + HPow.hPow (α := R) (β := ℕ) 0 2 * W.a₂ + HPow.hPow (α := R) (β := ℕ) 0 3 - 0 * W.a₃ -
          HPow.hPow (α := R) (β := ℕ) 0 2 -
        HMul.hMul (α := R) 0 0 * W.a₁) =
    W.a₆

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).a₁ = (↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).a₂ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).a₃ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).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)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).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:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
simp :
  HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s)) 2 +
      4 * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2)) =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂ + 12 * C.r)
⊢ (C • W).b₂ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.b₂ + 12 * C.r)

Tactic:
simp only [b₂, variableChange_a₁, variableChange_a₂]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.b₂, WeierstrassCurve.variableChange_a₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s)) 2 +
      4 * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2)) =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂ + 12 * C.r)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
simp :
  2 *
        (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)) +
      (↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s) * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 *
      (2 * W.a₄ + W.a₁ * W.a₃ + C.r * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) + 6 * HPow.hPow (β := ℕ) C.r 2)
⊢ (C • W).b₄ = HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 * (W.b₄ + C.r * W.b₂ + 6 * HPow.hPow (β := ℕ) C.r 2)

Tactic:
simp only [b₂, b₄, variableChange_a₁, variableChange_a₃, variableChange_a₄]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.variableChange_a₃, WeierstrassCurve.variableChange_a₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ 2 *
        (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)) +
      (↑C.u⁻¹ : R) * (W.a₁ + 2 * C.s) * (HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 *
      (2 * W.a₄ + W.a₁ * W.a₃ + C.r * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) + 6 * HPow.hPow (β := ℕ) C.r 2)

Tactic:
ring1