awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ (↑{
            u :=
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
                C.u,
            r :=
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                      t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                  HPow.hPow (β := ℕ) (↑C.u : R) 2 +
                C.r,
            s :=
              (↑C.u : R) *
                  { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                      t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
                C.s,
            t :=
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                        t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
                    HPow.hPow (β := ℕ) (↑C.u : R) 3 +
                  { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                          t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                      C.s *
                    HPow.hPow (β := ℕ) (↑C.u : R) 2 +
                C.t :
            VariableChange R }.u :
      R) =
    (↑(u { u := 1, r := 0, s := 0, t := 0 }) : R)
have u : (↑(C.u⁻¹ * C.u) : R) = (↑1 : R)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ {
        u :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
            C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
              HPow.hPow (β := ℕ) (↑C.u : R) 2 +
            C.r,
        s :=
          (↑C.u : R) *
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
                HPow.hPow (β := ℕ) (↑C.u : R) 3 +
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                      t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                  C.s *
                HPow.hPow (β := ℕ) (↑C.u : R) 2 +
            C.t :
        VariableChange R }.r =
    r { u := 1, r := 0, s := 0, t := 0 }
have r : -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * HPow.hPow (β := ℕ) (↑C.u : R) 2 + C.r = 0
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ {
        u :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
            C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
              HPow.hPow (β := ℕ) (↑C.u : R) 2 +
            C.r,
        s :=
          (↑C.u : R) *
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
                HPow.hPow (β := ℕ) (↑C.u : R) 3 +
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                      t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                  C.s *
                HPow.hPow (β := ℕ) (↑C.u : R) 2 +
            C.t :
        VariableChange R }.s =
    s { u := 1, r := 0, s := 0, t := 0 }
have s : (↑C.u : R) * (-C.s * (↑C.u⁻¹ : R)) + C.s = 0
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ {
        u :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.u *
            C.u,
        r :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
              HPow.hPow (β := ℕ) (↑C.u : R) 2 +
            C.r,
        s :=
          (↑C.u : R) *
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                  t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.s +
            C.s,
        t :=
          { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                    t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.t *
                HPow.hPow (β := ℕ) (↑C.u : R) 3 +
              { u := C.u⁻¹, r := -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2, s := -C.s * (↑C.u⁻¹ : R),
                      t := (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 : VariableChange R }.r *
                  C.s *
                HPow.hPow (β := ℕ) (↑C.u : R) 2 +
            C.t :
        VariableChange R }.t =
    t { u := 1, r := 0, s := 0, t := 0 }
have t : (C.r * C.s - C.t) * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * HPow.hPow (β := ℕ) (↑C.u : R) 3 +
      -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * C.s * HPow.hPow (β := ℕ) (↑C.u : R) 2 +
    C.t =
  0
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ HSMul.hSMul (α := VariableChange R) 1 W = W
have 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
Tactic: rw [VariableChange.one_def, variableChange_def, inv_one, Units.val_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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 (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₁
have a₁ : 1 * (W.a₁ + HMul.hMul (α := R) 2 0) = W.a₁
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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 (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₂
have a₂ : HPow.hPow (α := R) (β := ℕ) 1 2 * (W.a₂ - 0 * W.a₁ + HMul.hMul (α := R) 3 0 - HPow.hPow (α := R) (β := ℕ) 0 2) = W.a₂
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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 (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₃
have a₃ : HPow.hPow (α := R) (β := ℕ) 1 3 * (W.a₃ + 0 * W.a₁ + HMul.hMul (α := R) 2 0) = W.a₃
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange (goal)
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 (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₄
have 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₄
Tactic: dsimp only