awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
pos :
  { a := 1,
      b :=
        -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 -
            W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
          W.a₂,
      c :=
        2 * x₁ *
              HPow.hPow (β := ℕ)
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
            (W.a₁ * x₁ - 2 * y₁ - W.a₃) *
              ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 *
              HPow.hPow (β := ℕ)
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) *
              ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1,
      b :=
        -(x₁ + x₁ +
            W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))),
      c :=
        x₁ * x₁ +
            x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
          x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
      d :=
        -(x₁ * x₁ *
            W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }
⊢ { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 - W.a₁ * W.slope x₁ x₁ y₁ y₁ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₁ y₁ y₁ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₁ y₁ y₁ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₁ + W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)),
      c := x₁ * x₁ + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁) + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁),
      d := -(x₁ * x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) }

Tactic:
rw [slope_of_Y_ne rfl hy]

Premises used: WeierstrassCurve.Affine.slope_of_Y_ne, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
⊢ y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0

Tactic:
rw [negY, ← sub_ne_zero] at hy

Premises used: sub_ne_zero, WeierstrassCurve.Affine.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0
⊢ y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0

Tactic:
hy
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0
h : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) = y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)
⊢ y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0

Tactic:
convert! hy using 1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0
⊢ y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) = y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)

Tactic:
ring
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0
⊢ y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0

Tactic:
replace hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0 := by convert! hy using 1; ring
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ { a := 1,
        b :=
          -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
                  2 -
              W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            W.a₂,
        c :=
          2 * x₁ *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (W.a₁ * x₁ - 2 * y₁ - W.a₃) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -HPow.hPow (β := ℕ) x₁ 2 *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
        Cubic F }.a =
    { a := 1,
        b :=
          -(x₁ + x₁ +
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))),
        c :=
          x₁ * x₁ +
              x₁ *
                W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
        d :=
          -(x₁ * x₁ *
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }.a

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
pos :
  -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 -
        W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
      W.a₂ =
    -(x₁ + x₁ +
        (HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
                W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
              W.a₂ -
            x₁ -
          x₁))
⊢ { a := 1,
        b :=
          -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
                  2 -
              W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            W.a₂,
        c :=
          2 * x₁ *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (W.a₁ * x₁ - 2 * y₁ - W.a₃) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -HPow.hPow (β := ℕ) x₁ 2 *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
        Cubic F }.b =
    { a := 1,
        b :=
          -(x₁ + x₁ +
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))),
        c :=
          x₁ * x₁ +
              x₁ *
                W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
        d :=
          -(x₁ * x₁ *
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }.b

Tactic:
simp only [addX]

Premises used: WeierstrassCurve.Affine.addX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 -
        W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
      W.a₂ =
    -(x₁ + x₁ +
        (HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
                W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
              W.a₂ -
            x₁ -
          x₁))

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
pos :
  (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
        (x₁ * 2 * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) +
          (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (x₁ * W.a₁ - 2 * y₁ - W.a₃)) +
      HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 * (-(W.a₁ * y₁) + W.a₄) =
    x₁ *
      ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
              (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
            W.a₂ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
          x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 +
        ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
                (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
              W.a₂ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
            x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
          x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2))
⊢ { a := 1,
        b :=
          -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
                  2 -
              W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            W.a₂,
        c :=
          2 * x₁ *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (W.a₁ * x₁ - 2 * y₁ - W.a₃) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -HPow.hPow (β := ℕ) x₁ 2 *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
        Cubic F }.c =
    { a := 1,
        b :=
          -(x₁ + x₁ +
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))),
        c :=
          x₁ * x₁ +
              x₁ *
                W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
        d :=
          -(x₁ * x₁ *
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }.c

Tactic:
simp [field]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
        (x₁ * 2 * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) +
          (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (x₁ * W.a₁ - 2 * y₁ - W.a₃)) +
      HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 * (-(W.a₁ * y₁) + W.a₄) =
    x₁ *
      ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
              (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
            W.a₂ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
          x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 +
        ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
                (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
              W.a₂ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
            x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
          x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2))

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
            (-(x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁)) +
              (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (2 * y₁ + W.a₃)) -
          HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 * (y₁ * (y₁ + W.a₃) - W.a₆) +
        y₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 * (y₁ + x₁ * W.a₁ + W.a₃) -
      (-(HPow.hPow (β := ℕ) x₁ 2 *
            ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
                    (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
                  W.a₂ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
                x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
              x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2)) +
        HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 * (x₁ * (x₁ * (x₁ + W.a₂) + W.a₄) + W.a₆)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆

Tactic:
rw [equation_iff] at h₁ h₂

Premises used: WeierstrassCurve.Affine.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
h₃ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
⊢ HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆

Tactic:
rw [equation_iff] at h₁ h₂

Premises used: WeierstrassCurve.Affine.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
h₃ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
h₄ :
  HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆
⊢ ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)

Tactic:
rw [equation_iff] at h₁ h₂

Premises used: WeierstrassCurve.Affine.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
h₃ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
h₄ :
  HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆
hxy₁ : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ ¬x₁ = x₂

Tactic:
rw [equation_iff] at h₁ h₂

Premises used: WeierstrassCurve.Affine.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
h₂ :
  HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
neg :
  { a := 1, b := -HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) + x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)),
      d := -(x₁ * x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) }
⊢ { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }

Tactic:
rw [slope_of_X_ne hx]

Premises used: WeierstrassCurve.Affine.slope_of_X_ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
h₂ :
  HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
neg :
  { a := 1, b := -HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1,
      b :=
        -(x₁ + x₂ + (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)),
      c :=
        x₁ * x₂ +
            x₁ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂) +
          x₂ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂),
      d :=
        -(x₁ * x₂ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) }
⊢ { a := 1, b := -HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) + x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)),
      d := -(x₁ * x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) }

Tactic:
simp only [addX]

Premises used: WeierstrassCurve.Affine.addX