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₁ 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₂
⊢ { 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₂)) }

Tactic:
grind
-- 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 :
  (C : (a : F[X]) → F[X][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]))) =
    -HMul.hMul (β := F[X][Y])
        (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) : F[X][Y]))
        ((C : (a : F[X]) → F[X][Y])
            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X])) :
          F[X][Y])
⊢ (C : (a : F[X]) → F[X][Y]) (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) =
    -HMul.hMul (β := F[X][Y])
        (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) : F[X][Y]))
        ((C : (a : F[X]) → F[X][Y])
            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X])) :
          F[X][Y])

Tactic:
rw [addPolynomial_slope h₁ h₂ hxy]

Premises used: WeierstrassCurve.Affine.addPolynomial_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
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (C : (a : F[X]) → F[X][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]))) =
    -HMul.hMul (β := F[X][Y])
        (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) : F[X][Y]))
        ((C : (a : F[X]) → F[X][Y])
            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X])) :
          F[X][Y])

Tactic:
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 :
  (derivative : (a : F[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]) 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]))
⊢ (derivative : (a : F[X]) → F[X]) (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]) 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]))

Tactic:
rw [addPolynomial_slope h₁ h₂ hxy]

Premises used: WeierstrassCurve.Affine.addPolynomial_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
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
derivative_simp :
  -((HSub.hSub (α := F[X]) 1 0 * 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]) 1 0) *
          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]) x₂ : F[X]) *
          HSub.hSub (α := F[X]) 1 0) =
    -(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]))
⊢ (derivative : (a : F[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]) 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]))

Tactic:
derivative_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₂)
⊢ -((HSub.hSub (α := F[X]) 1 0 * 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]) 1 0) *
          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]) x₂ : F[X]) *
          HSub.hSub (α := F[X]) 1 0) =
    -(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]))

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx : eval (W'.addX x₁ x₂ ℓ) ((derivative : (a : R[X]) → R[X]) (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0
rw :
  evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (HSub.hSub (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
            Y)
          ((C : (a : R[X]) → R[X][Y])
              (HAdd.hAdd (β := R[X])
                ((C : (a : R) → R[X]) 3 * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (2 * W'.a₂) : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₄ : R[X])) :
            R[X][Y])) ≠
      0 ∨
    evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (HAdd.hAdd (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 2) : R[X][Y]) 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])) ≠
      0
⊢ W'.Nonsingular (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)

Tactic:
rw [Nonsingular, and_iff_right hx', negAddY, polynomialX, polynomialY]

Premises used: and_iff_right, WeierstrassCurve.Affine.polynomialY, WeierstrassCurve.Affine.Nonsingular, WeierstrassCurve.Affine.negAddY, WeierstrassCurve.Affine.polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx : eval (W'.addX x₁ x₂ ℓ) ((derivative : (a : R[X]) → R[X]) (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0
eval_simp :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
        (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) ≠
      0 ∨
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) ≠ 0
⊢ evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (HSub.hSub (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
            Y)
          ((C : (a : R[X]) → R[X][Y])
              (HAdd.hAdd (β := R[X])
                ((C : (a : R) → R[X]) 3 * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (2 * W'.a₂) : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₄ : R[X])) :
            R[X][Y])) ≠
      0 ∨
    evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (HAdd.hAdd (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 2) : R[X][Y]) 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])) ≠
      0

Tactic:
eval_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx : eval (W'.addX x₁ x₂ ℓ) ((derivative : (a : R[X]) → R[X]) (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0
contrapose! :
  ∀
    (hx :
      W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
            (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) =
          0 ∧
        2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0),
    eval (W'.addX x₁ x₂ ℓ) ((derivative : (a : R[X]) → R[X]) (W'.addPolynomial x₁ y₁ ℓ)) = 0
⊢ W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
        (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) ≠
      0 ∨
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) ≠ 0

Tactic:
contrapose! hx
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
        (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) =
      0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
eval_simp :
  eval (W'.addX x₁ x₂ ℓ)
      ((derivative : (a : R[X]) → R[X])
        (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]))) =
    0
⊢ eval (W'.addX x₁ x₂ ℓ)
      ((derivative : (a : R[X]) → R[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:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
        (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) =
      0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
eval_simp :
  2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) * ℓ +
        (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) * ℓ) -
      ((↑3 : R) * W'.addX x₁ x₂ ℓ ^ HSub.hSub (α := ℕ) 3 1 + W'.a₂ * (2 * W'.addX x₁ x₂ ℓ) + W'.a₄) =
    0
⊢ eval (W'.addX x₁ x₂ ℓ)
      (HMul.hMul (β := R[X])
            ((C : (a : R) → R[X]) 2 *
              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]))
            ((C : (a : R) → R[X]) ℓ : R[X]) +
          (HMul.hMul (α := R[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])) +
            HMul.hMul (β := R[X])
              (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]))
              ((C : (a : R) → R[X]) ℓ : R[X])) -
        HAdd.hAdd (β := R[X])
          ((C : (a : R) → R[X]) (↑3 : R) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 3 1) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X])
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X))
          ((C : (a : R) → R[X]) W'.a₄ : R[X])) =
    0

Tactic:
eval_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
        (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) =
      0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
a :
  2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) * ℓ +
            (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) * ℓ) -
          (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + W'.a₂ * (2 * W'.addX x₁ x₂ ℓ) + W'.a₄) +
        (0 + ℓ * 0) -
      (0 +
        (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
            (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) +
          ℓ * (2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃)))) =
    0
⊢ 2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) * ℓ +
            (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) * ℓ) -
          ((↑3 : R) * W'.addX x₁ x₂ ℓ ^ HSub.hSub (α := ℕ) 3 1 + W'.a₂ * (2 * W'.addX x₁ x₂ ℓ) + W'.a₄) +
        (0 + ℓ * 0) -
      (0 +
        (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
            (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) +
          ℓ * (2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃)))) =
    0

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
        (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) =
      0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
⊢ 2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) * ℓ +
            (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) * ℓ) -
          (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + W'.a₂ * (2 * W'.addX x₁ x₂ ℓ) + W'.a₄) +
        (0 + ℓ * 0) -
      (0 +
        (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
            (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) +
          ℓ * (2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃)))) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
        (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) =
      0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
a :
  2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) * ℓ +
            (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) * ℓ) -
          ((↑3 : R) * W'.addX x₁ x₂ ℓ ^ HSub.hSub (α := ℕ) 3 1 + W'.a₂ * (2 * W'.addX x₁ x₂ ℓ) + W'.a₄) +
        (0 + ℓ * 0) -
      (0 +
        (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) -
            (3 * HPow.hPow (β := ℕ) (W'.addX x₁ x₂ ℓ) 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) +
          ℓ * (2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃)))) =
    0
⊢ 2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) * ℓ +
        (W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) * ℓ) -
      ((↑3 : R) * W'.addX x₁ x₂ ℓ ^ HSub.hSub (α := ℕ) 3 1 + W'.a₂ * (2 * W'.addX x₁ x₂ ℓ) + W'.a₄) =
    0

Tactic:
linear_combination (norm := (norm_num1; ring1)) hx.left + ℓ * hx.right

Premises used: And.right, And.left