awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ Y -
        HSub.hSub (β := R[X][Y])
          (-HAdd.hAdd (β := R[X][Y])
                (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) ℓ) : R[X][Y])
                  (HSub.hSub (α := R[X][Y]) (β := R[X][Y])
                    ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ)) : R[X][Y])
                    ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) x₁) : R[X][Y])))
                ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y₁) : 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])
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ)) : R[X][Y]))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y]) +
      HSub.hSub (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ)) : R[X][Y]) *
        HAdd.hAdd (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) ℓ) : R[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]) W'.a₁) : R[X][Y])
            ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y]) +
        HAdd.hAdd (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) ℓ) : R[X][Y])
            (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
              ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) x₁) : R[X][Y])))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y₁) : R[X][Y]) +
      Y

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
e_s :
  HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y) : R[X][Y]) +
      HMul.hMul (α := R[X][Y]) (β := R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (-ℓ)) : R[X][Y]) =
    HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
      ((C : (a : R[X]) → R[X][Y])
          (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])) :
        R[X][Y])
⊢ Eq (α := Ideal W'.CoordinateRing)
    (span
      (insert (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
            ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))) :
          W'.CoordinateRing)
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
                  ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y) : R[X][Y]) +
                HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                  ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) :
                    R[X][Y])
                  ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (-ℓ)) : R[X][Y])) :
            W'.CoordinateRing))))
    (span
      (insert (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
            ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))) :
          W'.CoordinateRing)
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
                ((C : (a : R[X]) → R[X][Y])
                    (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])) :
                  R[X][Y])) :
            W'.CoordinateRing))))

Tactic:
congr 4
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
e_s :
  HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y) : R[X][Y]) +
      HMul.hMul (β := R[X][Y])
        (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) x) : R[X][Y]))
        (-(C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) ℓ) : R[X][Y]) =
    Y -
      HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) ℓ) : R[X][Y])
          (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
            ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) x) : R[X][Y])))
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y) : R[X][Y])
⊢ HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y) : R[X][Y]) +
      HMul.hMul (α := R[X][Y]) (β := R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (-ℓ)) : R[X][Y]) =
    HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
      ((C : (a : R[X]) → R[X][Y])
          (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])) :
        R[X][Y])

Tactic:
C_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
⊢ HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y) : R[X][Y]) +
      HMul.hMul (β := R[X][Y])
        (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) x) : R[X][Y]))
        (-(C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) ℓ) : R[X][Y]) =
    Y -
      HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) ℓ) : R[X][Y])
          (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
            ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) x) : R[X][Y])))
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) y) : R[X][Y])

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂), y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
neg : ∀ (hx : ¬x₁ = x₂), y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
by_cases hx : x₁ = x₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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.Point
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₁),
    y₁ = eval x₁ (linePolynomial x₁ y₁ (W.slope x₁ x₁ y₁ y₁))
⊢ y₂ = eval x₂ (linePolynomial x₁ y₁ (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.Point
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₁
⊢ y₁ = eval x₁ (linePolynomial x₁ y₁ (W.slope x₁ x₁ y₁ y₁))

Tactic:
simp [linePolynomial]

Premises used: WeierstrassCurve.Affine.linePolynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂
neg : y₂ * (x₁ - x₂) = (y₁ - y₂) * (x₂ - x₁) + (x₁ - x₂) * y₁
⊢ y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
simp [field, linePolynomial, slope_of_X_ne hx, sub_ne_zero_of_ne hx]

Premises used: WeierstrassCurve.Affine.slope_of_X_ne, sub_ne_zero_of_ne, WeierstrassCurve.Affine.linePolynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂ * (x₁ - x₂) = (y₁ - y₂) * (x₂ - x₁) + (x₁ - x₂) * y₁

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂)
⊢ y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
have hy₂ : y₂ = (linePolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂).eval x₂ := by
    by_cases hx : x₁ = x₂
    · have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩
      rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩
      simp [linePolynomial]
    · simp [field, linePolynomial, slope_of_X_ne hx, sub_ne_zero_of_ne hx]
      ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
nth_rw :
  Eq (α := Ideal W.CoordinateRing)
    (XYIdeal W x₂ ((C : (a : F) → F[X]) (eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))))
    (XYIdeal W x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))
⊢ Eq (α := Ideal W.CoordinateRing) (XYIdeal W x₂ ((C : (a : F) → F[X]) y₂))
    (XYIdeal W x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))

Tactic:
nth_rw 1 [hy₂]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
e_s :
  HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂ * (x₂ - x₁) + y₁)) : 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]) ((C : (a : F) → F[X]) (-W.slope x₁ x₂ y₁ y₂)) : F[X][Y]) =
    HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
      ((C : (a : F[X]) → F[X][Y])
          (HAdd.hAdd (β := F[X])
            (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
              (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
            ((C : (a : F) → F[X]) y₁ : F[X])) :
        F[X][Y])
⊢ HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
        ((C : (a : F[X]) → F[X][Y])
            ((C : (a : F) → F[X])
              (eval x₂
                (HAdd.hAdd (β := F[X])
                  (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
                    (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
                  ((C : (a : F) → F[X]) y₁ : F[X])))) :
          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]) ((C : (a : F) → F[X]) (-W.slope x₁ x₂ y₁ y₂)) : F[X][Y]) =
    HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
      ((C : (a : F[X]) → F[X][Y])
          (HAdd.hAdd (β := F[X])
            (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
              (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
            ((C : (a : F) → F[X]) y₁ : F[X])) :
        F[X][Y])

Tactic:
simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul]

Premises used: Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_mul, Polynomial.eval_add, Polynomial.eval_sub
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
e_s :
  Y -
        HAdd.hAdd (β := F[X][Y])
          (HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])
            (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y])
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])))
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y₁) : F[X][Y]) +
      HMul.hMul (β := F[X][Y])
        (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y]))
        (-(C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂)) : F[X][Y]) =
    Y -
      HAdd.hAdd (β := F[X][Y])
        (HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])
          (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])))
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y₁) : F[X][Y])
⊢ HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂ * (x₂ - x₁) + y₁)) : 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]) ((C : (a : F) → F[X]) (-W.slope x₁ x₂ y₁ y₂)) : F[X][Y]) =
    HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
      ((C : (a : F[X]) → F[X][Y])
          (HAdd.hAdd (β := F[X])
            (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
              (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
            ((C : (a : F) → F[X]) y₁ : F[X])) :
        F[X][Y])

Tactic:
C_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
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₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ Y -
        HAdd.hAdd (β := F[X][Y])
          (HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])
            (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y])
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])))
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y₁) : F[X][Y]) +
      HMul.hMul (β := F[X][Y])
        (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y]))
        (-(C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂)) : F[X][Y]) =
    Y -
      HAdd.hAdd (β := F[X][Y])
        (HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂)) : F[X][Y])
          (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])))
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y₁) : F[X][Y])

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
a :
  HAdd.hAdd (β := F[X][Y])
        (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
            HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]) -
          HMul.hMul (α := 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])
            (HSub.hSub (α := F[X][Y])
              ((C : (a : F[X]) → F[X][Y])
                  (HAdd.hAdd (β := F[X])
                    (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                      HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                    ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
                F[X][Y])
              (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y]) Y)))
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y)) :
          F[X][Y]) -
      HAdd.hAdd (β := F[X][Y]) (HMul.hMul (α := F[X][Y]) W.polynomial 1)
        ((C : (a : F[X]) → F[X][Y])
            ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆)) :
          F[X][Y]) =
    0
⊢ HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]) -
      HMul.hMul (α := 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])
        (HSub.hSub (α := F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              (HAdd.hAdd (β := F[X])
                (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
            F[X][Y])
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
            Y)) =
    HMul.hMul (α := F[X][Y]) W.polynomial 1

Tactic:
linear_combination (norm := (rw [negY, polynomial]; C_simp; ring1))
      congr_arg C (congr_arg C ((equation_iff ..).mp h.left).symm)

Premises used: Polynomial.C, WeierstrassCurve.Affine.polynomial, congr_arg, WeierstrassCurve.Affine.negY, And.left, WeierstrassCurve.Affine.equation_iff, Iff.mp, Eq.symm, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]) -
      HMul.hMul (α := 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])
        (HSub.hSub (α := F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              (HAdd.hAdd (β := F[X])
                (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
            F[X][Y])
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
            Y)) =
    HMul.hMul (α := F[X][Y]) W.polynomial 1

Tactic:
have Y_rw : (Y - C (C y)) * (Y - C (C <| W.negY x y)) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
        W.polynomial * 1 := by
    linear_combination (norm := (rw [negY, polynomial]; C_simp; ring1))
      congr_arg C (congr_arg C ((equation_iff ..).mp h.left).symm)
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]) -
      HMul.hMul (α := 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])
        (HSub.hSub (α := F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              (HAdd.hAdd (β := F[X])
                (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
            F[X][Y])
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
            Y)) =
    HMul.hMul (α := F[X][Y]) W.polynomial 1
⊢ HMul.hMul (α := Ideal W.CoordinateRing)
      (span
        (singleton (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))) :
            W.CoordinateRing)))
      ⊤ =
    span
      (singleton (α := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing)
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))) :
          W.CoordinateRing))

Tactic:
mul_top (_ : Ideal W.CoordinateRing)

Premises used: Ideal.mul_top
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y]) -
      HMul.hMul (α := 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])
        (HSub.hSub (α := F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              (HAdd.hAdd (β := F[X])
                (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
            F[X][Y])
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
            Y)) =
    HMul.hMul (α := F[X][Y]) W.polynomial 1
⊢ IsTwoSided (α := W.CoordinateRing)
    (span
      (singleton (α := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing)
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))) :
          W.CoordinateRing)))

Tactic:
infer_instance