awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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
⊢ 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
have 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
Tactic: eval_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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
⊢ 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
have 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
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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 (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
have 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
Tactic: eval_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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 (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
have 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
Tactic: eval_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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 : 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
have 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
Tactic: norm_num1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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 : R) * W'.addX x₁ x₂ ℓ ^ HSub.hSub (α := ℕ) 3 1 + W'.a₂ * (2 * W'.addX x₁ x₂ ℓ) + W'.a₄) =
    0
have 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
Tactic: linear_combination (norm := (norm_num1; ring1)) hx.left + ℓ * hx.right
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔ eval (W'.addX x₁ x₂ ℓ) (W'.addPolynomial x₁ y₁ ℓ) = 0
have 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
Tactic: rw [Equation, negAddY, addPolynomial, linePolynomial, polynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (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₂)
⊢ W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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
Tactic: rw [equation_add_iff, addPolynomial_slope h₁ h₂ hxy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (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₂)
⊢ 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
have 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
Tactic: eval_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (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₂)
⊢ -((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
have 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
Tactic: rw [neg_eq_zero, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (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₂)
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
⊢ -((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
have 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
Tactic: rw [neg_eq_zero, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (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₂)
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
⊢ -((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
have rw₂ : Eq.{u + 1} (α := F) 0 0
Tactic: rw [neg_eq_zero, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₂))
Tactic: by_cases hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₂))
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₂))
Tactic: by_cases hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₁
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₁)
Tactic: rwa [negAddY, hx₁, sub_self, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₁)
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have pos₁ : W.Nonsingular x₁ (W.slope x₁ x₂ y₁ y₂ * (x₁ - x₁) + y₁)
Tactic: rwa [negAddY, hx₁, sub_self, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₁)
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have pos₂ : W.Nonsingular x₁ (W.slope x₁ x₂ y₁ y₂ * 0 + y₁)
Tactic: rwa [negAddY, hx₁, sub_self, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₁)
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have pos₃ : W.Nonsingular x₁ (0 + y₁)
Tactic: rwa [negAddY, hx₁, sub_self, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₁
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₂))
Tactic: by_cases hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₂))
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₂))
Tactic: by_cases hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₂))
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₂))
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₂))
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₂))
Tactic: subst hx
Cleared hypotheses: x₂, h₂, hxy, hx₁, hx₂, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
have 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₁)
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]