awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ Eq (α := Ideal W'.CoordinateRing) (XYIdeal W' (W'.addX x₁ x₂ ℓ) ((C : (a : R) → R[X]) (W'.addY x₁ x₂ y₁ ℓ)))
    (span
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
                ((C : (a : R[X]) → R[X][Y]) (linePolynomial x₁ y₁ ℓ) : R[X][Y])) :
            W'.CoordinateRing)) ⊔
      XIdeal W' (W'.addX x₁ x₂ ℓ))
have simp : 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]) (W'.addX 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]) (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) :
                R[X][Y])) :
          W'.CoordinateRing))))
  (span
      (singleton (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
            (HSub.hSub (β := 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]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                      ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
                  R[X][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)) ⊔
    span
      (singleton (α := 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]) (W'.addX x₁ x₂ ℓ) : R[X]))) :
          W'.CoordinateRing)))
Tactic: simp only [XYIdeal, XIdeal, XClass, YClass, addY, negAddY, negY, negPolynomial, linePolynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
        ((C : (a : R[X]) → R[X][Y])
            ((C : (a : R) → R[X]) (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) :
          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]) (W'.addX x₁ x₂ ℓ) : R[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]) (β := 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])
        ((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]) +
      Y
have e_s : 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: C_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
⊢ 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])) :
            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))))
have rw : 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: rw [← span_pair_add_left_mul _ _ <| mk W' <| C <| C <| -ℓ, ← map_mul, ← map_add]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
⊢ 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))))
have 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])
Tactic: congr 4
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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]) (β := 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])
have 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])
Tactic: C_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂))
have pos : ∀ (hx : x₁ = x₂), y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂))
⊢ y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
have neg : ∀ (hx : ¬x₁ = x₂), y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
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₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
have hy : y₁ ≠ W.negY x₂ y₂
Tactic: have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂
⊢ y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₁))
Tactic: rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩
Cleared hypotheses: x₂, y₂, h₂, hxy, hx, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
have neg : y₂ * (x₁ - x₂) = (y₁ - y₂) * (x₂ - x₁) + (x₁ - x₂) * y₁
Tactic: simp [field, linePolynomial, slope_of_X_ne hx, sub_ne_zero_of_ne hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
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₂)
⊢ 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₂)))
have hy₂ : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂))
⊢ 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₂)))
have 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₂)))
Tactic: nth_rw 1 [hy₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂))
⊢ 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])
have 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])
Tactic: simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂))
⊢ 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])
have 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])
Tactic: C_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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
have 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
Tactic: linear_combination (norm := (rw [negY, polynomial]; C_simp; ring1))
      congr_arg C (congr_arg C ((equation_iff ..).mp h.left).symm)