awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
rw :
  evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (HSub.hSub (β := R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
            HMul.hMul (α := R[X][Y]) (β := R[X][Y])
              ((C : (a : R[X]) → R[X][Y])
                  (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])) :
                R[X][Y])
              Y)
          ((C : (a : R[X]) → R[X][Y])
              (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])) :
            R[X][Y])) =
      0 ↔
    eval (W'.addX x₁ x₂ ℓ)
        (eval
          (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]))
          (HSub.hSub (β := R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
              HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                ((C : (a : R[X]) → R[X][Y])
                    (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])) :
                  R[X][Y])
                Y)
            ((C : (a : R[X]) → R[X][Y])
                (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])) :
              R[X][Y]))) =
      0
⊢ W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔ eval (W'.addX x₁ x₂ ℓ) (W'.addPolynomial x₁ y₁ ℓ) = 0

Tactic:
rw [Equation, negAddY, addPolynomial, linePolynomial, polynomial]

Premises used: WeierstrassCurve.Affine.polynomial, WeierstrassCurve.Affine.Equation, WeierstrassCurve.Affine.addPolynomial, WeierstrassCurve.Affine.negAddY, WeierstrassCurve.Affine.linePolynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (HSub.hSub (β := R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
            HMul.hMul (α := R[X][Y]) (β := R[X][Y])
              ((C : (a : R[X]) → R[X][Y])
                  (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])) :
                R[X][Y])
              Y)
          ((C : (a : R[X]) → R[X][Y])
              (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])) :
            R[X][Y])) =
      0 ↔
    eval (W'.addX x₁ x₂ ℓ)
        (eval
          (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]))
          (HSub.hSub (β := R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
              HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                ((C : (a : R[X]) → R[X][Y])
                    (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])) :
                  R[X][Y])
                Y)
            ((C : (a : R[X]) → R[X][Y])
                (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])) :
              R[X][Y]))) =
      0

Tactic:
eval_simp
-- 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 :
  eval (W.addX x₁ x₂ (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]))) =
    0
⊢ W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
rw [equation_add_iff, addPolynomial_slope h₁ h₂ hxy]

Premises used: WeierstrassCurve.Affine.addPolynomial_slope, WeierstrassCurve.Affine.equation_add_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₂)
eval_simp :
  -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) =
    0
⊢ eval (W.addX x₁ x₂ (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]))) =
    0

Tactic:
eval_simp
-- 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 :
  (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
      (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) =
    0
rw₁ : (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) * 0 = 0
rw₂ rw₃ : Eq.{u + 1} (α := F) 0 0
⊢ -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) =
    0

Tactic:
rw [neg_eq_zero, sub_self, mul_zero]

Premises used: sub_self, neg_eq_zero, MulZeroClass.mul_zero
-- 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₂)
⊢ W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
(equation_neg ..).mpr <| equation_negAdd h₁ h₂ hxy

Premises used: Iff.mpr, WeierstrassCurve.Affine.equation_neg, WeierstrassCurve.Affine.addY, WeierstrassCurve.Affine.equation_negAdd
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
pos :
  ∀ (hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁),
    W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
neg :
  ∀ (hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁),
    W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
by_cases hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁

Premises used: WeierstrassCurve.Affine.slope, WeierstrassCurve.Affine.addX
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
pos :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + y₁)
pos₁ : W.Nonsingular x₁ (W.slope x₁ x₂ y₁ y₂ * (x₁ - x₁) + y₁)
pos₂ : W.Nonsingular x₁ (W.slope x₁ x₂ y₁ y₂ * 0 + y₁)
pos₃ : W.Nonsingular x₁ (0 + y₁)
pos₄ pos₅ pos₆ pos₇ : W.Nonsingular x₁ y₁
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
rwa [negAddY, hx₁, sub_self, mul_zero, zero_add]

Premises used: sub_self, zero_add, MulZeroClass.mul_zero, WeierstrassCurve.Affine.negAddY
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
pos :
  ∀ (hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂),
    W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
neg :
  ∀ (hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂),
    W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
by_cases hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂

Premises used: WeierstrassCurve.Affine.slope, WeierstrassCurve.Affine.addX
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
pos : ∀ (hx : x₁ = x₂), W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
neg : ∀ (hx : ¬x₁ = x₂), W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : x₁ = x₂
pos :
  ∀ (h₂ : W.Nonsingular x₁ y₂) (hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₂)) (hx₁ : ¬W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₂) = x₁)
    (hx₂ : W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₂) = x₁),
    W.Nonsingular (W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₂)) (W.negAddY x₁ x₁ y₁ (W.slope x₁ x₁ y₁ y₂))
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
subst hx
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₁ y₂
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₂)
hx₁ : ¬W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₂) = x₁
⊢ W.Nonsingular (W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₂)) (W.negAddY x₁ x₁ y₁ (W.slope x₁ x₁ y₁ y₂))

Tactic:
contradiction
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : ¬x₁ = x₂
neg :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + y₁)
neg₁ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * -(x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₁)
neg₂ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + y₁)
neg₃ : W.Nonsingular x₂ (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - x₂)) + y₁)
neg₄ : W.Nonsingular x₂ (-((y₁ - y₂) / (x₁ - x₂) * (x₁ - x₂)) + y₁)
neg₅ : W.Nonsingular x₂ (-(y₁ - y₂) + y₁)
neg₆ : W.Nonsingular x₂ (y₂ - y₁ + y₁)
neg₇ neg₈ neg₉ neg₁₀ : W.Nonsingular x₂ y₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
rwa [negAddY, ← neg_sub, mul_neg, hx₂, slope_of_X_ne hx,
          div_mul_cancel₀ _ <| sub_ne_zero_of_ne hx, neg_sub, sub_add_cancel]

Premises used: div_mul_cancel₀, neg_sub, WeierstrassCurve.Affine.slope_of_X_ne, sub_ne_zero_of_ne, WeierstrassCurve.Affine.negAddY, sub_add_cancel, mul_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
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
neg :
  eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
      ((derivative : (a : F[X]) → F[X]) (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) ≠
    0
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
apply nonsingular_negAdd_of_eval_derivative_ne_zero <| equation_negAdd h₁.left h₂.left hxy

Premises used: And.left, WeierstrassCurve.Affine.equation_negAdd, WeierstrassCurve.Affine.nonsingular_negAdd_of_eval_derivative_ne_zero
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
neg :
  eval (W.addX x₁ x₂ (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]) 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]) +
          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]))) ≠
    0
⊢ eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
      ((derivative : (a : F[X]) → F[X]) (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) ≠
    0

Tactic:
rw [derivative_addPolynomial_slope h₁.left h₂.left hxy]

Premises used: WeierstrassCurve.Affine.derivative_addPolynomial_slope, And.left
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
neg :
  -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) +
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) *
            (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) ≠
    0
⊢ eval (W.addX x₁ x₂ (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]) 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]) +
          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]))) ≠
    0

Tactic:
eval_simp
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
neg : (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) ≠ 0
⊢ -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) +
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) *
            (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) ≠
    0

Tactic:
simp only [neg_ne_zero, sub_self, mul_zero, add_zero]

Premises used: sub_self, MulZeroClass.mul_zero, neg_ne_zero, add_zero
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
⊢ (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) ≠ 0

Tactic:
mul_ne_zero (sub_ne_zero_of_ne hx₁) (sub_ne_zero_of_ne hx₂)

Premises used: sub_ne_zero_of_ne, mul_ne_zero
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
⊢ (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) ≠ 0

Tactic:
exact mul_ne_zero (sub_ne_zero_of_ne hx₁) (sub_ne_zero_of_ne hx₂)

Premises used: sub_ne_zero_of_ne, mul_ne_zero
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
(nonsingular_neg ..).mpr <| nonsingular_negAdd h₁ h₂ hxy

Premises used: WeierstrassCurve.Affine.nonsingular_negAdd, Iff.mpr, WeierstrassCurve.Affine.addY, WeierstrassCurve.Affine.nonsingular_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₂
simp_rw :
  -(x₁ - (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂)) - x₂ =
    -(x₁ -
            (HPow.hPow (β := ℕ) ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) 2 +
                W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) -
              W.a₂)) -
        x₂ -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / HPow.hPow (β := ℕ) (x₁ - x₂) 2
⊢ W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) =
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) -
      (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / HPow.hPow (β := ℕ) (x₂ - x₁) 2

Tactic:
simp_rw [slope_of_X_ne hx, addX, negY, ← neg_sub x₁, neg_sq]

Premises used: neg_sub, neg_sq, WeierstrassCurve.Affine.slope_of_X_ne, WeierstrassCurve.Affine.negY, WeierstrassCurve.Affine.addX
-- 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₂
simp :
  (y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) / HPow.hPow (β := ℕ) (x₁ - x₂) 2 - W.a₂ - x₁ - x₂ =
    (y₁ - (-y₂ - x₂ * W.a₁ - W.a₃)) * (y₁ - (-y₂ - x₂ * W.a₁ - W.a₃) + (x₁ - x₂) * W.a₁) /
              HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            W.a₂ -
          x₁ -
        x₂ -
      (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (y₂ - (-y₂ - x₂ * W.a₁ - W.a₃)) / HPow.hPow (β := ℕ) (x₁ - x₂) 2
⊢ -(x₁ - (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂)) - x₂ =
    -(x₁ -
            (HPow.hPow (β := ℕ) ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) 2 +
                W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) -
              W.a₂)) -
        x₂ -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / HPow.hPow (β := ℕ) (x₁ - x₂) 2

Tactic:
simp [field]
-- 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₂
⊢ (y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) / HPow.hPow (β := ℕ) (x₁ - x₂) 2 - W.a₂ - x₁ - x₂ =
    (y₁ - (-y₂ - x₂ * W.a₁ - W.a₃)) * (y₁ - (-y₂ - x₂ * W.a₁ - W.a₃) + (x₁ - x₂) * W.a₁) /
              HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            W.a₂ -
          x₁ -
        x₂ -
      (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (y₂ - (-y₂ - x₂ * W.a₁ - W.a₃)) / HPow.hPow (β := ℕ) (x₁ - x₂) 2

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
hx : x₁ ≠ x₂
simp_rw :
  y₁ * (x₂ - (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) +
        y₂ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
      ((y₁ - y₂) / (x₁ - x₂) *
            (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
          y₁) *
        (x₁ - x₂) =
    0
⊢ let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂);
  y₁ * (x₂ - x₃) + y₂ * (x₃ - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0

Tactic:
simp_rw [slope_of_X_ne hx, negAddY, addX]

Premises used: WeierstrassCurve.Affine.slope_of_X_ne, WeierstrassCurve.Affine.addX, WeierstrassCurve.Affine.negAddY
-- 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₂
simp :
  y₁ *
          (x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - HPow.hPow (β := ℕ) (x₁ - x₂) 2 * W.a₂ -
                x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
              x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2)) +
        y₂ *
          ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - HPow.hPow (β := ℕ) (x₁ - x₂) 2 * W.a₂ -
                x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
              x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2) +
      ((y₁ - y₂) *
          ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - HPow.hPow (β := ℕ) (x₁ - x₂) 2 * W.a₂ -
                x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
              x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2) +
        y₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 3) =
    0
⊢ y₁ * (x₂ - (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) +
        y₂ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
      ((y₁ - y₂) / (x₁ - x₂) *
            (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
          y₁) *
        (x₁ - x₂) =
    0

Tactic:
simp [field, sub_ne_zero.mpr hx]

Premises used: Iff.mpr, sub_ne_zero