awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
r :
  (x.r * HPow.hPow (β := ℕ) (↑x_1.u : R) 2 + x_1.r) * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 + x_2.r =
    x.r * HPow.hPow (β := ℕ) ((↑x_1.u : R) * (↑x_2.u : R)) 2 + (x_1.r * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 + x_2.r)
⊢ (x * x_1 * x_2).r = (x * (x_1 * x_2)).r

Tactic:
simp only [mul_def, Units.val_mul]

Premises used: WeierstrassCurve.VariableChange.mul_def, Units.val_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
s :
  (↑x_2.u : R) * ((↑x_1.u : R) * x.s + x_1.s) + x_2.s =
    (↑x_1.u : R) * (↑x_2.u : R) * x.s + ((↑x_2.u : R) * x_1.s + x_2.s)
⊢ (x * x_1 * x_2).s = (x * (x_1 * x_2)).s

Tactic:
simp only [mul_def, Units.val_mul]

Premises used: WeierstrassCurve.VariableChange.mul_def, Units.val_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
t :
  (x.t * HPow.hPow (β := ℕ) (↑x_1.u : R) 3 + x.r * x_1.s * HPow.hPow (β := ℕ) (↑x_1.u : R) 2 + x_1.t) *
          HPow.hPow (β := ℕ) (↑x_2.u : R) 3 +
        (x.r * HPow.hPow (β := ℕ) (↑x_1.u : R) 2 + x_1.r) * x_2.s * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 +
      x_2.t =
    x.t * HPow.hPow (β := ℕ) ((↑x_1.u : R) * (↑x_2.u : R)) 3 +
        x.r * ((↑x_2.u : R) * x_1.s + x_2.s) * HPow.hPow (β := ℕ) ((↑x_1.u : R) * (↑x_2.u : R)) 2 +
      (x_1.t * HPow.hPow (β := ℕ) (↑x_2.u : R) 3 + x_1.r * x_2.s * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 + x_2.t)
⊢ (x * x_1 * x_2).t = (x * (x_1 * x_2)).t

Tactic:
simp only [mul_def, Units.val_mul]

Premises used: WeierstrassCurve.VariableChange.mul_def, Units.val_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
⊢ (↑x.u : R) * (↑x_1.u : R) * (↑x_2.u : R) = (↑x.u : R) * ((↑x_1.u : R) * (↑x_2.u : R))

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
⊢ (x.r * HPow.hPow (β := ℕ) (↑x_1.u : R) 2 + x_1.r) * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 + x_2.r =
    x.r * HPow.hPow (β := ℕ) ((↑x_1.u : R) * (↑x_2.u : R)) 2 + (x_1.r * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 + x_2.r)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
⊢ (↑x_2.u : R) * ((↑x_1.u : R) * x.s + x_1.s) + x_2.s =
    (↑x_1.u : R) * (↑x_2.u : R) * x.s + ((↑x_2.u : R) * x_1.s + x_2.s)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C C' x x_1 x_2 : VariableChange R
⊢ (x.t * HPow.hPow (β := ℕ) (↑x_1.u : R) 3 + x.r * x_1.s * HPow.hPow (β := ℕ) (↑x_1.u : R) 2 + x_1.t) *
          HPow.hPow (β := ℕ) (↑x_2.u : R) 3 +
        (x.r * HPow.hPow (β := ℕ) (↑x_1.u : R) 2 + x_1.r) * x_2.s * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 +
      x_2.t =
    x.t * HPow.hPow (β := ℕ) ((↑x_1.u : R) * (↑x_2.u : R)) 3 +
        x.r * ((↑x_2.u : R) * x_1.s + x_2.s) * HPow.hPow (β := ℕ) ((↑x_1.u : R) * (↑x_2.u : R)) 2 +
      (x_1.t * HPow.hPow (β := ℕ) (↑x_2.u : R) 3 + x_1.r * x_2.s * HPow.hPow (β := ℕ) (↑x_2.u : R) 2 + x_2.t)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ 1 * C = C

Tactic:
simp only [mul_def, one_def, zero_add, zero_mul, mul_zero, one_mul]

Premises used: MulZeroClass.zero_mul, WeierstrassCurve.VariableChange.mul_def, zero_add, MulZeroClass.mul_zero, WeierstrassCurve.VariableChange.one_def, one_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ C * 1 = C

Tactic:
simp only [mul_def, one_def, add_zero, mul_zero, one_mul, mul_one, one_pow, Units.val_one]

Premises used: one_pow, WeierstrassCurve.VariableChange.mul_def, MulZeroClass.mul_zero, WeierstrassCurve.VariableChange.one_def, Units.val_one, mul_one, add_zero, one_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
rw :
  {
      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 := 1, r := 0, s := 0, t := 0 }
⊢ C⁻¹ * C = 1

Tactic:
rw [mul_def, one_def, inv_def]

Premises used: WeierstrassCurve.VariableChange.mul_def, WeierstrassCurve.VariableChange.inv_def, WeierstrassCurve.VariableChange.one_def
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
u : (↑(C.u⁻¹ * C.u) : R) = (↑1 : 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) =
    (↑(VariableChange.u { u := 1, r := 0, s := 0, t := 0 }) : R)

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
r : -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * HPow.hPow (β := ℕ) (↑C.u : R) 2 + C.r = 0
⊢ {
        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 =
    VariableChange.r { u := 1, r := 0, s := 0, t := 0 }

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
s : (↑C.u : R) * (-C.s * (↑C.u⁻¹ : R)) + C.s = 0
⊢ {
        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 =
    VariableChange.s { u := 1, r := 0, s := 0, t := 0 }

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
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
⊢ {
        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 =
    VariableChange.t { u := 1, r := 0, s := 0, t := 0 }

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ (↑(C.u⁻¹ * C.u) : R) = (↑1 : R)

Tactic:
C.u.inv_mul

Premises used: Units.inv_mul, WeierstrassCurve.VariableChange.u
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ (↑(C.u⁻¹ * C.u) : R) = (↑1 : R)

Tactic:
exact C.u.inv_mul

Premises used: Units.inv_mul, WeierstrassCurve.VariableChange.u
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ -C.r * HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * HPow.hPow (β := ℕ) (↑C.u : R) 2 + C.r = 0

Tactic:
linear_combination -C.r * pow_mul_pow_eq_one 2 C.u.inv_mul

Premises used: WeierstrassCurve.VariableChange.r, Units.inv_mul, WeierstrassCurve.VariableChange.u, pow_mul_pow_eq_one, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ (↑C.u : R) * (-C.s * (↑C.u⁻¹ : R)) + C.s = 0

Tactic:
linear_combination -C.s * C.u.inv_mul

Premises used: Units.inv_mul, WeierstrassCurve.VariableChange.u, WeierstrassCurve.VariableChange.s
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
C_1 C' C : VariableChange R
⊢ (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:
linear_combination (C.r * C.s - C.t) * pow_mul_pow_eq_one 3 C.u.inv_mul
        + -C.r * C.s * pow_mul_pow_eq_one 2 C.u.inv_mul

Premises used: WeierstrassCurve.VariableChange.r, HMul.hMul, HSub.hSub, Units.inv_mul, WeierstrassCurve.VariableChange.u, WeierstrassCurve.VariableChange.s, WeierstrassCurve.VariableChange.t, pow_mul_pow_eq_one, OfNat.ofNat
-- 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),
      a₂ := HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - HPow.hPow (β := ℕ) C.s 2),
      a₃ := HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t),
      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),
      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_1 : WeierstrassCurve R
C_1 C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ : R) * (↑C'.u⁻¹ : R) * (W.a₁ + 2 * ((↑C'.u : R) * C.s + C'.s)) =
    (↑C.u⁻¹ : R) * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s) + 2 * C.s)

Tactic:
linear_combination ↑C.u⁻¹ * C.s * 2 * C'.u.inv_mul

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

Tactic:
linear_combination
        C.s * (-C'.s * 2 - W.a₁) * C.u⁻¹ ^ 2 * ↑C'.u⁻¹ * C'.u.inv_mul
          + (C.r * 3 - C.s ^ 2) * C.u⁻¹ ^ 2 * pow_mul_pow_eq_one 2 C'.u.inv_mul

Premises used: WeierstrassCurve.VariableChange.r, HMul.hMul, HSub.hSub, Units.inv_mul, WeierstrassCurve.VariableChange.u, WeierstrassCurve.VariableChange.s, HPow.hPow, pow_mul_pow_eq_one, OfNat.ofNat, Neg.neg, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C_1 C C' : VariableChange R
W : WeierstrassCurve R
⊢ HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (↑C'.u⁻¹ : R)) 3 *
      (W.a₃ + (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * W.a₁ +
        2 * (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t)) =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 3 *
      (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t) +
          C.r * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s)) +
        2 * C.t)

Tactic:
linear_combination
        C.r * (C'.s * 2 + W.a₁) * C.u⁻¹ ^ 3 * ↑C'.u⁻¹ * pow_mul_pow_eq_one 2 C'.u.inv_mul
          + C.t * 2 * C.u⁻¹ ^ 3 * pow_mul_pow_eq_one 3 C'.u.inv_mul

Premises used: WeierstrassCurve.VariableChange.r, HMul.hMul, Units.inv_mul, WeierstrassCurve.VariableChange.u, WeierstrassCurve.VariableChange.s, WeierstrassCurve.VariableChange.t, HAdd.hAdd, pow_mul_pow_eq_one, OfNat.ofNat, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C_1 C C' : VariableChange R
W : WeierstrassCurve R
⊢ HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (↑C'.u⁻¹ : R)) 4 *
      (W.a₄ - ((↑C'.u : R) * C.s + C'.s) * W.a₃ + 2 * (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * W.a₂ -
            (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t +
                (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * ((↑C'.u : R) * C.s + C'.s)) *
              W.a₁ +
          3 * HPow.hPow (β := ℕ) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) 2 -
        2 * ((↑C'.u : R) * C.s + C'.s) *
          (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t)) =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 4 *
      (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.s * (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) +
              2 * C.r *
                (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - HPow.hPow (β := ℕ) C'.s 2)) -
            (C.t + C.r * C.s) * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s)) +
          3 * HPow.hPow (β := ℕ) C.r 2 -
        2 * C.s * C.t)

Tactic:
linear_combination
        C.s * (-W.a₃ - C'.r * W.a₁ - C'.t * 2) * C.u⁻¹ ^ 4 * C'.u⁻¹ ^ 3 * C'.u.inv_mul
          + C.u⁻¹ ^ 4 * C'.u⁻¹ ^ 2 * (C.r * C'.r * 6 + C.r * W.a₂ * 2 - C'.s * C.r * W.a₁ * 2
            - C'.s ^ 2 * C.r * 2) * pow_mul_pow_eq_one 2 C'.u.inv_mul
          - C.u⁻¹ ^ 4 * ↑C'.u⁻¹ * (C.s * C'.s * C.r * 2 + C.s * C.r * W.a₁ + C'.s * C.t * 2
            + C.t * W.a₁) * pow_mul_pow_eq_one 3 C'.u.inv_mul
          + C.u⁻¹ ^ 4 * (C.r ^ 2 * 3 - C.s * C.t * 2) * pow_mul_pow_eq_one 4 C'.u.inv_mul

Premises used: WeierstrassCurve.VariableChange.r, HMul.hMul, HSub.hSub, Units.inv_mul, WeierstrassCurve.VariableChange.u, WeierstrassCurve.a₂, WeierstrassCurve.a₃, WeierstrassCurve.VariableChange.s, WeierstrassCurve.VariableChange.t, HPow.hPow, HAdd.hAdd, pow_mul_pow_eq_one, OfNat.ofNat, Neg.neg, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
Goal:
R : Type u
inst : CommRing R
W_1 : WeierstrassCurve R
C_1 C C' : VariableChange R
W : WeierstrassCurve R
⊢ HPow.hPow (β := ℕ) ((↑C.u⁻¹ : R) * (↑C'.u⁻¹ : R)) 6 *
      (W.a₆ + (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) * W.a₄ +
                HPow.hPow (β := ℕ) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) 2 * W.a₂ +
              HPow.hPow (β := ℕ) (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) 3 -
            (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) * W.a₃ -
          HPow.hPow (β := ℕ)
            (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) 2 -
        (C.r * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.r) *
            (C.t * HPow.hPow (β := ℕ) (↑C'.u : R) 3 + C.r * C'.s * HPow.hPow (β := ℕ) (↑C'.u : R) 2 + C'.t) *
          W.a₁) =
    HPow.hPow (β := ℕ) (↑C.u⁻¹ : R) 6 *
      (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₁) +
                  C.r *
                    (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)) +
                HPow.hPow (β := ℕ) C.r 2 *
                  (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - HPow.hPow (β := ℕ) C'.s 2)) +
              HPow.hPow (β := ℕ) C.r 3 -
            C.t * (HPow.hPow (β := ℕ) (↑C'.u⁻¹ : R) 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) -
          HPow.hPow (β := ℕ) C.t 2 -
        C.r * C.t * ((↑C'.u⁻¹ : R) * (W.a₁ + 2 * C'.s)))

Tactic:
linear_combination
        C.r * C.u⁻¹ ^ 6 * C'.u⁻¹ ^ 4 * (C'.r * W.a₂ * 2 - C'.r * C'.s * W.a₁ + C'.r ^ 2 * 3 + W.a₄
            - C'.s * C'.t * 2 - C'.s * W.a₃ - C'.t * W.a₁) * pow_mul_pow_eq_one 2 C'.u.inv_mul
          - C.u⁻¹ ^ 6 * C'.u⁻¹ ^ 3 * C.t * (C'.r * W.a₁ + C'.t * 2 + W.a₃)
            * pow_mul_pow_eq_one 3 C'.u.inv_mul
          + C.r ^ 2 * C.u⁻¹ ^ 6 * C'.u⁻¹ ^ 2 * (C'.r * 3 + W.a₂ - C'.s * W.a₁ - C'.s ^ 2)
            * pow_mul_pow_eq_one 4 C'.u.inv_mul
          - C.r * C.t * C.u⁻¹ ^ 6 * ↑C'.u⁻¹ * (C'.s * 2 + W.a₁) * pow_mul_pow_eq_one 5 C'.u.inv_mul
          + C.u⁻¹ ^ 6 * (C.r ^ 3 - C.t ^ 2) * pow_mul_pow_eq_one 6 C'.u.inv_mul

Premises used: WeierstrassCurve.VariableChange.r, HMul.hMul, HSub.hSub, Units.inv_mul, WeierstrassCurve.VariableChange.u, WeierstrassCurve.a₂, WeierstrassCurve.a₃, WeierstrassCurve.VariableChange.s, WeierstrassCurve.VariableChange.t, HPow.hPow, HAdd.hAdd, WeierstrassCurve.a₄, pow_mul_pow_eq_one, OfNat.ofNat, WeierstrassCurve.a₁