awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
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₁)
⊢ 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₂ * -(x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₁)
Tactic: rwa [negAddY, ← neg_sub, mul_neg, hx₂, slope_of_X_ne hx,
          div_mul_cancel₀ _ <| sub_ne_zero_of_ne hx, neg_sub, sub_add_cancel]
-- 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₂
neg :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + y₁)
neg₁ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * -(x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₁)
⊢ 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₂ * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + y₁)
Tactic: rwa [negAddY, ← neg_sub, mul_neg, hx₂, slope_of_X_ne hx,
          div_mul_cancel₀ _ <| sub_ne_zero_of_ne hx, neg_sub, sub_add_cancel]
-- 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₂
neg :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + y₁)
neg₁ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * -(x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₁)
neg₂ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + y₁)
⊢ 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 x₂ (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - 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]
-- 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₂
neg :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + y₁)
neg₁ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * -(x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₁)
neg₂ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + y₁)
neg₃ : W.Nonsingular x₂ (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - x₂)) + y₁)
⊢ 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 x₂ (-((y₁ - y₂) / (x₁ - x₂) * (x₁ - 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]
-- 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₂
neg :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + y₁)
neg₁ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * -(x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₁)
neg₂ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + y₁)
neg₃ : W.Nonsingular x₂ (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - x₂)) + y₁)
neg₄ : W.Nonsingular x₂ (-((y₁ - y₂) / (x₁ - x₂) * (x₁ - x₂)) + y₁)
⊢ 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 x₂ (-(y₁ - y₂) + y₁)
Tactic: rwa [negAddY, ← neg_sub, mul_neg, hx₂, slope_of_X_ne hx,
          div_mul_cancel₀ _ <| sub_ne_zero_of_ne hx, neg_sub, sub_add_cancel]
-- 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₂
neg :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + y₁)
neg₁ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * -(x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₁)
neg₂ :
  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + y₁)
neg₃ : W.Nonsingular x₂ (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - x₂)) + y₁)
neg₄ : W.Nonsingular x₂ (-((y₁ - y₂) / (x₁ - x₂) * (x₁ - x₂)) + y₁)
neg₅ : W.Nonsingular x₂ (-(y₁ - y₂) + y₁)
⊢ 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 x₂ (y₂ - y₁ + y₁)
Tactic: rwa [negAddY, ← neg_sub, mul_neg, hx₂, slope_of_X_ne hx,
          div_mul_cancel₀ _ <| sub_ne_zero_of_ne hx, neg_sub, sub_add_cancel]
-- 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 neg : eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    ((derivative : (a : F[X]) → F[X]) (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) ≠
  0
Tactic: apply nonsingular_negAdd_of_eval_derivative_ne_zero <| equation_negAdd h₁.left h₂.left 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.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₂
⊢ eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
      ((derivative : (a : F[X]) → F[X]) (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) ≠
    0
have neg : eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (-(HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X]) *
            HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]) +
          HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X]) *
            HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X]) +
        HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]) *
          HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X]))) ≠
  0
Tactic: rw [derivative_addPolynomial_slope h₁.left h₂.left 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.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₂
⊢ eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
      (-(HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X]) *
              HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]) +
            HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X]) *
              HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X]) +
          HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]) *
            HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X]))) ≠
    0
have neg : -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) +
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) *
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
      (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) ≠
  0
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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
⊢ -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) +
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) *
            (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) ≠
    0
have neg : (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) ≠ 0
Tactic: simp only [neg_ne_zero, sub_self, mul_zero, add_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
hx : x₁ ≠ x₂
⊢ W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) =
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) -
      (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / HPow.hPow (β := ℕ) (x₂ - x₁) 2
have simp_rw : -(x₁ - (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂)) - x₂ =
  -(x₁ -
          (HPow.hPow (β := ℕ) ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) 2 +
              W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) -
            W.a₂)) -
      x₂ -
    (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / HPow.hPow (β := ℕ) (x₁ - x₂) 2
Tactic: simp_rw [slope_of_X_ne hx, addX, negY, ← neg_sub x₁, neg_sq]
-- 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
hx : x₁ ≠ x₂
⊢ -(x₁ - (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂)) - x₂ =
    -(x₁ -
            (HPow.hPow (β := ℕ) ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) 2 +
                W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) -
              W.a₂)) -
        x₂ -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / HPow.hPow (β := ℕ) (x₁ - x₂) 2
have simp : (y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) / HPow.hPow (β := ℕ) (x₁ - x₂) 2 - W.a₂ - x₁ - x₂ =
  (y₁ - (-y₂ - x₂ * W.a₁ - W.a₃)) * (y₁ - (-y₂ - x₂ * W.a₁ - W.a₃) + (x₁ - x₂) * W.a₁) /
            HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
          W.a₂ -
        x₁ -
      x₂ -
    (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (y₂ - (-y₂ - x₂ * W.a₁ - W.a₃)) / HPow.hPow (β := ℕ) (x₁ - x₂) 2
Tactic: simp [field]
-- 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
hx : x₁ ≠ x₂
⊢ let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂);
  y₁ * (x₂ - x₃) + y₂ * (x₃ - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0
have simp_rw : y₁ * (x₂ - (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) +
      y₂ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
    ((y₁ - y₂) / (x₁ - x₂) *
          (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
        y₁) *
      (x₁ - x₂) =
  0
Tactic: simp_rw [slope_of_X_ne hx, negAddY, addX]
-- 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
hx : x₁ ≠ x₂
⊢ y₁ * (x₂ - (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) +
        y₂ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
      ((y₁ - y₂) / (x₁ - x₂) *
            (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
          y₁) *
        (x₁ - x₂) =
    0
have simp : y₁ *
        (x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
          ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - HPow.hPow (β := ℕ) (x₁ - x₂) 2 * W.a₂ -
              x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2)) +
      y₂ *
        ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - HPow.hPow (β := ℕ) (x₁ - x₂) 2 * W.a₂ -
              x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
          x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2) +
    ((y₁ - y₂) *
        ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - HPow.hPow (β := ℕ) (x₁ - x₂) 2 * W.a₂ -
              x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
          x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2) +
      y₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 3) =
  0
Tactic: simp [field, sub_ne_zero.mpr 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
hx : x₁ ≠ x₂
⊢ let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂);
  let y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂);
  y₃ - W.negY x₃ y₃ = ((y₂ - W.negY x₂ y₂) * (x₁ - x₃) - (y₁ - W.negY x₁ y₁) * (x₂ - x₃)) / (x₂ - x₁)
have simp_rw : (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
      (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
          W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
        W.a₃)) *
    (x₂ - x₁) =
  (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
    (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
Tactic: simp_rw [addY, negY, eq_div_iff (sub_ne_zero.mpr hx.symm)]
-- 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
hx : x₁ ≠ x₂
⊢ (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
        (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
            W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
          W.a₃)) *
      (x₂ - x₁) =
    (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
have a : (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
          (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
              W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
            W.a₃)) *
        (x₂ - x₁) +
      HMul.hMul (α := F) 2 0 -
    ((y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
        (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
      2 *
        (y₁ * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) +
          W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂))) =
  0
Tactic: linear_combination (norm := ring1) 2 * cyclic_sum_Y_mul_X_sub_X y₁ y₂ hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x y : R
⊢ (W'.map f).negY ((f : (a : R) → S) x) ((f : (a : R) → S) y) = (f : (a : R) → S) (W'.negY x y)
have simp : HSub.hSub (α := S) (-(f : (a : R) → S) y : S) (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) x : S)) -
    (W'.map f).a₃ =
  (f : (a : R) → S) (-y - W'.a₁ * x - W'.a₃)
Tactic: simp only [negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x y ℓ : R
⊢ (W'.map f).addPolynomial ((f : (a : R) → S) x) ((f : (a : R) → S) y) ((f : (a : R) → S) ℓ) =
    Polynomial.map f (W'.addPolynomial x y ℓ)
have rw : eval₂ (mapRingHom f)
    (HAdd.hAdd (β := S[X])
      (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) ℓ) : S[X])
        (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) ((f : (a : R) → S) x) : S[X])))
      ((C : (a : S) → S[X]) ((f : (a : R) → S) y) : S[X]))
    W'.polynomial =
  eval₂ (mapRingHom f)
    ((mapRingHom f : (a : R[X]) → S[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])))
    W'.polynomial
Tactic: rw [addPolynomial, map_polynomial, eval_map, linePolynomial, addPolynomial, ← coe_mapRingHom,
    ← eval₂_hom, linePolynomial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x₁ x₂ ℓ : R
⊢ (W'.map f).addX ((f : (a : R) → S) x₁) ((f : (a : R) → S) x₂) ((f : (a : R) → S) ℓ) =
    (f : (a : R) → S) (W'.addX x₁ x₂ ℓ)
have simp : HSub.hSub (β := S)
    (HSub.hSub (β := S)
      (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) ℓ : S) 2 +
          HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) ℓ : S) -
        (W'.map f).a₂)
      ((f : (a : R) → S) x₁ : S))
    ((f : (a : R) → S) x₂ : S) =
  (f : (a : R) → S) (HPow.hPow (β := ℕ) ℓ 2 + W'.a₁ * ℓ - W'.a₂ - x₁ - x₂)
Tactic: simp only [addX]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x₁ y₁ x₂ ℓ : R
⊢ (W'.map f).negAddY ((f : (a : R) → S) x₁) ((f : (a : R) → S) x₂) ((f : (a : R) → S) y₁) ((f : (a : R) → S) ℓ) =
    (f : (a : R) → S) (W'.negAddY x₁ x₂ y₁ ℓ)
have simp : HAdd.hAdd (β := S)
    (HMul.hMul (α := S) ((f : (a : R) → S) ℓ : S)
      (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) (W'.addX x₁ x₂ ℓ) : S) ((f : (a : R) → S) x₁ : S)))
    ((f : (a : R) → S) y₁ : S) =
  (f : (a : R) → S) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
Tactic: simp only [negAddY, map_addX]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
have pos : ∀ (hx : x₁ = x₂),
  (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (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
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
pos :
  ∀ (hx : x₁ = x₂),
    (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
      (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
have neg : ∀ (hx : ¬x₁ = x₂),
  (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (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
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
have pos : ∀ (hy : y₁ = W.negY x₂ y₂),
  (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
Tactic: by_cases hy : y₁ = W.negY x₂ y₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
pos :
  ∀ (hy : y₁ = W.negY x₂ y₂),
    (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
      (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
have neg : ∀ (hy : ¬y₁ = W.negY x₂ y₂),
  (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
Tactic: by_cases hy : y₁ = W.negY x₂ y₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
⊢ (f : (a : F) → K) y₁ = (W.map f).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)
have rw : (f : (a : F) → K) (W.negY x₂ y₂) = (W.map f).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)
Tactic: rw [hy, map_negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
rw : (f : (a : F) → K) (W.negY x₂ y₂) = (W.map f).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)
⊢ (f : (a : F) → K) y₁ = (W.map f).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)
have rw₁ : Eq.{v + 1} (α := K) ((f : (a : F) → K) (W.negY x₂ y₂) : K) ((f : (a : F) → K) (W.negY x₂ y₂) : K)
Tactic: rw [hy, map_negY]