awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine 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₆
hx : x₁ = x₂
rw : (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) = 0
⊢ y₁ = y₂ ∨ y₁ = W.negY x₂ y₂

Tactic:
rw [← sub_eq_zero, ← sub_eq_zero (a := y₁), ← mul_eq_zero, negY]

Premises used: sub_eq_zero, mul_eq_zero, WeierstrassCurve.Affine.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine 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₆
hx : x₁ = x₂
a :
  (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) +
        (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₂)) -
      (0 +
        (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₆))) =
    0
⊢ (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) +
        (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₂)) -
      (0 +
        (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₆))) =
    0

Tactic:
rw [hx]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine 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₆
hx : x₁ = x₂
⊢ (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) +
        (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₂)) -
      (0 +
        (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₆))) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine 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₆
hx : x₁ = x₂
a :
  (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) +
        (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₂)) -
      (0 +
        (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₆))) =
    0
⊢ (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) = 0

Tactic:
linear_combination (norm := (rw [hx]; ring1)) h₁ - h₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ y₁ = y₂

Tactic:
(Y_eq_of_X_eq h₁ h₂ hx).resolve_right hy

Premises used: WeierstrassCurve.Affine.Y_eq_of_X_eq, Or.resolve_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
rw :
  HPow.hPow (β := ℕ) (-y - W'.a₁ * x - W'.a₃) 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) +
        W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
      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₆
⊢ W'.Equation x (W'.negY x y) ↔ W'.Equation x y

Tactic:
rw [equation_iff, equation_iff, negY]

Premises used: WeierstrassCurve.Affine.negY, WeierstrassCurve.Affine.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
a :
  HPow.hPow (β := ℕ) (-y - W'.a₁ * x - W'.a₃) 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) +
      W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
    HPow.hPow (β := ℕ) y 2 + W'.a₁ * x * y + W'.a₃ * y
⊢ HPow.hPow (β := ℕ) (-y - W'.a₁ * x - W'.a₃) 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) +
        W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
      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:
congr! 1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
⊢ HPow.hPow (β := ℕ) (-y - W'.a₁ * x - W'.a₃) 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) +
      W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
    HPow.hPow (β := ℕ) y 2 + W'.a₁ * x * y + W'.a₃ * y

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
rw :
  W'.Equation x y ∧ (W'.a₁ * W'.negY x y ≠ 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ W'.negY x y) ↔
    W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ -y - W'.a₁ * x - W'.a₃)
⊢ W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y

Tactic:
rw [nonsingular_iff, equation_neg, ← negY, negY_negY, ← @ne_comm _ y, nonsingular_iff]

Premises used: WeierstrassCurve.Affine.equation_neg, WeierstrassCurve.Affine.negY, ne_comm, WeierstrassCurve.Affine.negY_negY, WeierstrassCurve.Affine.nonsingular_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
h : y = W'.negY x y
rw rw₁ :
  W'.a₁ * y = 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ↔
    W'.a₁ * y = 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄
⊢ W'.a₁ * W'.negY x y = 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ↔
    W'.a₁ * y = 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄

Tactic:
rw [← h]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ∧ (W'.a₁ * W'.negY x y ≠ 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ W'.negY x y) ↔
    W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ -y - W'.a₁ * x - W'.a₃)

Tactic:
exact and_congr_right' <| (iff_congr not_and_or.symm not_and_or.symm).mpr <|
    not_congr <| and_congr_left fun h => by rw [← h]

Premises used: Iff.mpr, and_congr_right', iff_congr, and_congr_left, not_and_or, Iff.symm, not_congr
-- 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
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
rw :
  (if x₁ = x₂ then
      if y₁ = W.negY x₂ y₂ then 0
      else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
    else (y₁ - y₂) / (x₁ - x₂)) =
    0
rw₁ :
  (if y₁ = W.negY x₂ y₂ then 0
    else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) =
    0
rw₂ rw₃ : Eq.{u + 1} (α := F) 0 0
⊢ W.slope x₁ x₂ y₁ y₂ = 0

Tactic:
rw [slope, if_pos hx, if_pos hy]

Premises used: WeierstrassCurve.Affine.slope, if_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₂ y₁ y₂ : F
hy : ¬y₁ = -y₂ - W.a₁ * x₂ - W.a₃
⊢ W.slope x₂ x₂ y₁ y₂ =
    (3 * HPow.hPow (β := ℕ) x₂ 2 + 2 * W.a₂ * x₂ + W.a₄ - W.a₁ * y₁) / (y₁ - (-y₁ - W.a₁ * x₂ - W.a₃))

Tactic:
simp [slope, hy]

Premises used: WeierstrassCurve.Affine.slope
-- 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
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ W.slope x₁ x₂ y₁ y₂ = (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)

Tactic:
simp_all
-- 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
hx : x₁ ≠ x₂
rw :
  (if x₁ = x₂ then
      if y₁ = W.negY x₂ y₂ then 0
      else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
    else (y₁ - y₂) / (x₁ - x₂)) =
    (y₁ - y₂) / (x₁ - x₂)
rw₁ rw₂ : (y₁ - y₂) / (x₁ - x₂) = (y₁ - y₂) / (x₁ - x₂)
⊢ W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)

Tactic:
rw [slope, if_neg hx]

Premises used: WeierstrassCurve.Affine.slope, if_neg
-- 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
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
rw :
  (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
    (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / evalEval x₁ y₁ W.polynomialY
⊢ W.slope x₁ x₂ y₁ y₂ = -evalEval x₁ y₁ W.polynomialX / evalEval x₁ y₁ W.polynomialY

Tactic:
rw [slope_of_Y_ne hx hy, evalEval_polynomialX, neg_sub]

Premises used: neg_sub, WeierstrassCurve.Affine.slope_of_Y_ne, WeierstrassCurve.Affine.evalEval_polynomialX
-- 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
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
e_a : y₁ - W.negY x₁ y₁ = evalEval x₁ y₁ W.polynomialY
⊢ (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
    (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / evalEval x₁ y₁ W.polynomialY

Tactic:
congr 1
-- 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
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
e_a : y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) = 2 * y₁ + W.a₁ * x₁ + W.a₃
⊢ y₁ - W.negY x₁ y₁ = evalEval x₁ y₁ W.polynomialY

Tactic:
rw [negY, evalEval_polynomialY]

Premises used: WeierstrassCurve.Affine.negY, WeierstrassCurve.Affine.evalEval_polynomialY
-- 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
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) = 2 * y₁ + W.a₁ * x₁ + W.a₃

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
⊢ HPow.hPow (β := ℕ)
          (HAdd.hAdd (β := R[X])
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
            ((C : (a : R) → R[X]) y : R[X]))
          2 +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₃ : R[X]) *
          HAdd.hAdd (β := R[X])
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
            ((C : (a : R) → R[X]) y : R[X]) -
      HAdd.hAdd (β := R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
        ((C : (a : R) → R[X]) W'.a₆ : R[X]) =
    -(1 * HPow.hPow (α := R[X]) (β := ℕ) X 3 +
            HAdd.hAdd (β := R[X])
                (-HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) ℓ : R[X]) 2 -
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) ((C : (a : R) → R[X]) ℓ : R[X]))
                ((C : (a : R) → R[X]) W'.a₂ : R[X]) *
              HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          (HMul.hMul (α := R[X]) (β := R[X]) (2 : R[X]) ((C : (a : R) → R[X]) x : R[X]) *
                  HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) ℓ : R[X]) 2 +
                HMul.hMul (β := R[X])
                  (HSub.hSub (β := R[X])
                    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X])
                        ((C : (a : R) → R[X]) x : R[X]) -
                      HMul.hMul (α := R[X]) (β := R[X]) (2 : R[X]) ((C : (a : R) → R[X]) y : R[X]))
                    ((C : (a : R) → R[X]) W'.a₃ : R[X]))
                  ((C : (a : R) → R[X]) ℓ : R[X]) +
              HAdd.hAdd (β := R[X])
                (HMul.hMul (α := R[X]) (β := R[X]) (-(C : (a : R) → R[X]) W'.a₁ : R[X]) ((C : (a : R) → R[X]) y : R[X]))
                ((C : (a : R) → R[X]) W'.a₄ : R[X])) *
            X +
        (-HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) x : R[X]) 2 *
              HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) ℓ : R[X]) 2 +
            HMul.hMul (β := R[X])
              (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) (2 : R[X]) ((C : (a : R) → R[X]) x : R[X]))
                  ((C : (a : R) → R[X]) y : R[X]) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₃ : R[X]) ((C : (a : R) → R[X]) x : R[X]))
              ((C : (a : R) → R[X]) ℓ : R[X]) -
          HSub.hSub (β := R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) ((C : (a : R) → R[X]) y : R[X]) 2 +
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₃ : R[X]) ((C : (a : R) → R[X]) y : R[X]))
            ((C : (a : R) → R[X]) W'.a₆ : R[X])))

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₂)
rw :
  { 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₂)) }
⊢ W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
    -(HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X]) *
          HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]) *
        HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X]))

Tactic:
rw [addPolynomial_eq, neg_inj, Cubic.prod_X_sub_C_eq, Cubic.toPoly_injective]

Premises used: Cubic.toPoly_injective, WeierstrassCurve.Affine.addPolynomial_eq, Cubic.prod_X_sub_C_eq, neg_inj
-- 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₂)
pos :
  ∀ (hx : 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₂)) }
neg :
  ∀ (hx : ¬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₂)) }
⊢ { 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:
by_cases hx : x₁ = x₂
-- 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₂
⊢ y₁ ≠ W.negY x₂ y₂

Tactic:
have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩
-- 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₂
hy : y₁ ≠ W.negY x₂ y₂
pos :
  ∀ (h₂ : W.Equation x₁ y₁) (hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)) (hy : 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₁)) }
⊢ { 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:
rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩

Premises used: WeierstrassCurve.Affine.Y_eq_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₂ : W.Equation x₁ y₁
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
⊢ 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₁ y₁ : F
h₁ h₂ : W.Equation x₁ y₁
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
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₁ y₁ : F
h₁ h₂ : W.Equation x₁ y₁
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
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₆
⊢ ¬(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₁ y₁ : F
h₁ h₂ : W.Equation x₁ y₁
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
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₁)
⊢ y₁ ≠ W.negY x₁ y₁

Tactic:
rw [equation_iff] at h₁ h₂

Premises used: WeierstrassCurve.Affine.equation_iff