awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (hypothesis)
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hx : x₁ = x₂
⊢ y₁ = y₂ ∨ y₁ = W.negY x₂ y₂
have h₃ : HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
  HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
Tactic: rw [equation_iff] at h₁ h₂
Cleared hypotheses: h₁, h₂, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (hypothesis)
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hx : x₁ = x₂
h₃ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
⊢ y₁ = y₂ ∨ y₁ = W.negY x₂ y₂
have h₄ : HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
  HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆
Tactic: rw [equation_iff] at h₁ h₂
Cleared hypotheses: h₁, h₂, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
h₂ :
  HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆
hx : x₁ = x₂
⊢ y₁ = y₂ ∨ y₁ = W.negY x₂ y₂
have rw : (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) = 0
Tactic: rw [← sub_eq_zero, ← sub_eq_zero (a := y₁), ← mul_eq_zero, negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
h₂ :
  HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆
hx : x₁ = x₂
⊢ (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) +
        (HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆ +
          (HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂)) -
      (0 +
        (HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ +
          (HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆))) =
    0
have a : (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) +
      (HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆ +
        (HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂)) -
    (0 +
      (HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₂ * y₁ + W.a₃ * y₁ +
        (HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆))) =
  0
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
h₂ :
  HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆
hx : x₁ = x₂
⊢ (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) = 0
have a : (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) +
      (HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆ +
        (HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂)) -
    (0 +
      (HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ +
        (HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆))) =
  0
Tactic: linear_combination (norm := (rw [hx]; ring1)) h₁ - h₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x (W'.negY x y) ↔ W'.Equation x y
have rw : HPow.hPow (β := ℕ) (-y - W'.a₁ * x - W'.a₃) 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) +
      W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
    HPow.hPow (β := ℕ) x 3 + W'.a₂ * HPow.hPow (β := ℕ) x 2 + W'.a₄ * x + W'.a₆ ↔
  HPow.hPow (β := ℕ) y 2 + W'.a₁ * x * y + W'.a₃ * y =
    HPow.hPow (β := ℕ) x 3 + W'.a₂ * HPow.hPow (β := ℕ) x 2 + W'.a₄ * x + W'.a₆
Tactic: rw [equation_iff, equation_iff, negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
⊢ HPow.hPow (β := ℕ) (-y - W'.a₁ * x - W'.a₃) 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) +
        W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
      HPow.hPow (β := ℕ) x 3 + W'.a₂ * HPow.hPow (β := ℕ) x 2 + W'.a₄ * x + W'.a₆ ↔
    HPow.hPow (β := ℕ) y 2 + W'.a₁ * x * y + W'.a₃ * y =
      HPow.hPow (β := ℕ) x 3 + W'.a₂ * HPow.hPow (β := ℕ) x 2 + W'.a₄ * x + W'.a₆
have a : HPow.hPow (β := ℕ) (-y - W'.a₁ * x - W'.a₃) 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) +
    W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
  HPow.hPow (β := ℕ) y 2 + W'.a₁ * x * y + W'.a₃ * y
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
⊢ W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y
have rw : W'.Equation x y ∧ (W'.a₁ * W'.negY x y ≠ 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ W'.negY x y) ↔
  W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ -y - W'.a₁ * x - W'.a₃)
Tactic: rw [nonsingular_iff, equation_neg, ← negY, negY_negY, ← @ne_comm _ y, nonsingular_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
h : y = W'.negY x y
⊢ W'.a₁ * W'.negY x y = 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ↔
    W'.a₁ * y = 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄
have rw : W'.a₁ * y = 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄ ↔
  W'.a₁ * y = 3 * HPow.hPow (β := ℕ) x 2 + 2 * W'.a₂ * x + W'.a₄
Tactic: rw [← h]
-- 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₂
hy : y₁ = W.negY x₂ y₂
⊢ W.slope x₁ x₂ y₁ y₂ = 0
have rw : (if x₁ = x₂ then
    if y₁ = W.negY x₂ y₂ then 0
    else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
  else (y₁ - y₂) / (x₁ - x₂)) =
  0
Tactic: rw [slope, if_pos hx, if_pos hy]
-- 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₂
hy : y₁ = W.negY x₂ y₂
rw :
  (if x₁ = x₂ then
      if y₁ = W.negY x₂ y₂ then 0
      else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
    else (y₁ - y₂) / (x₁ - x₂)) =
    0
⊢ W.slope x₁ x₂ y₁ y₂ = 0
have rw₁ : (if y₁ = W.negY x₂ y₂ then 0
  else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) =
  0
Tactic: rw [slope, if_pos hx, if_pos hy]
-- 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₂
hy : y₁ = W.negY x₂ y₂
rw :
  (if x₁ = x₂ then
      if y₁ = W.negY x₂ y₂ then 0
      else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
    else (y₁ - y₂) / (x₁ - x₂)) =
    0
rw₁ :
  (if y₁ = W.negY x₂ y₂ then 0
    else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) =
    0
⊢ W.slope x₁ x₂ y₁ y₂ = 0
have rw₂ : Eq.{u + 1} (α := F) 0 0
Tactic: rw [slope, if_pos hx, if_pos hy]
-- 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.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)
have rw : (if x₁ = x₂ then
    if y₁ = W.negY x₂ y₂ then 0
    else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
  else (y₁ - y₂) / (x₁ - x₂)) =
  (y₁ - y₂) / (x₁ - x₂)
Tactic: rw [slope, if_neg 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₂
rw :
  (if x₁ = x₂ then
      if y₁ = W.negY x₂ y₂ then 0
      else (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
    else (y₁ - y₂) / (x₁ - x₂)) =
    (y₁ - y₂) / (x₁ - x₂)
⊢ W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)
have rw₁ : (y₁ - y₂) / (x₁ - x₂) = (y₁ - y₂) / (x₁ - x₂)
Tactic: rw [slope, if_neg 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₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ W.slope x₁ x₂ y₁ y₂ = -evalEval x₁ y₁ W.polynomialX / evalEval x₁ y₁ W.polynomialY
have rw : (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
  (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / evalEval x₁ y₁ W.polynomialY
Tactic: rw [slope_of_Y_ne hx hy, evalEval_polynomialX, neg_sub]
-- 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₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
    (3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / evalEval x₁ y₁ W.polynomialY
have e_a : y₁ - W.negY x₁ y₁ = evalEval x₁ y₁ W.polynomialY
Tactic: congr 1
-- 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₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ y₁ - W.negY x₁ y₁ = evalEval x₁ y₁ W.polynomialY
have e_a : y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) = 2 * y₁ + W.a₁ * x₁ + W.a₃
Tactic: rw [negY, evalEval_polynomialY]
-- 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.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
    -(HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X]) *
          HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]) *
        HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X]))
have rw : { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
    c :=
      2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ +
        (-W.a₁ * y₁ + W.a₄),
    d :=
      -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 +
          (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
        (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
    Cubic F } =
  { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
    c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
    d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }
Tactic: rw [addPolynomial_eq, neg_inj, Cubic.prod_X_sub_C_eq, Cubic.toPoly_injective]
-- 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₂)
⊢ { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }
have pos : ∀ (hx : x₁ = x₂),
  { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (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.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
pos :
  ∀ (hx : x₁ = x₂),
    { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
        c :=
          2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
            (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
        Cubic F } =
      { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
        c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
        d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }
⊢ { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }
have neg : ∀ (hx : ¬x₁ = x₂),
  { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }
Tactic: by_cases hx : x₁ = x₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (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₂
⊢ { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (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.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₂)
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₂ y₁ y₂) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (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₁),
  { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 - W.a₁ * W.slope x₁ x₁ y₁ y₁ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₁ y₁ y₁ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₁ y₁ y₁ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₁ + W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)),
      c := x₁ * x₁ + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁) + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁),
      d := -(x₁ * x₁ * W.addX x₁ x₁ (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.Formula (hypothesis)
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₁
⊢ { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 - W.a₁ * W.slope x₁ x₁ y₁ y₁ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₁ y₁ y₁ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₁ y₁ y₁ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₁ + W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)),
      c := x₁ * x₁ + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁) + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁),
      d := -(x₁ * x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) }
have h₃ : HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
  HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
Tactic: rw [equation_iff] at h₁ h₂
Cleared hypotheses: h₁, h₂, hxy, hy
-- 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₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
⊢ { a := 1, b := -HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 - W.a₁ * W.slope x₁ x₁ y₁ y₁ + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₁ y₁ y₁ +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) (W.slope x₁ x₁ y₁ y₁) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₁ y₁ y₁ -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₁ + W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)),
      c := x₁ * x₁ + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁) + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁),
      d := -(x₁ * x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) }
have pos : { a := 1,
    b :=
      -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 -
          W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
        W.a₂,
    c :=
      2 * x₁ *
            HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
              2 +
          (W.a₁ * x₁ - 2 * y₁ - W.a₃) *
            ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
        (-W.a₁ * y₁ + W.a₄),
    d :=
      -HPow.hPow (β := ℕ) x₁ 2 *
            HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
              2 +
          (2 * x₁ * y₁ + W.a₃ * x₁) *
            ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
        (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
    Cubic F } =
  { a := 1,
    b :=
      -(x₁ + x₁ +
          W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))),
    c :=
      x₁ * x₁ +
          x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
        x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
    d :=
      -(x₁ * x₁ *
          W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }
Tactic: rw [slope_of_Y_ne rfl hy]