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
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 (β := ℕ) ((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₁))) }
have hy₁ : y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0
Tactic: rw [negY, ← sub_ne_zero] at hy
Cleared hypotheses: 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₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0
⊢ y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
have h : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) = y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)
Tactic: convert! hy using 1
-- 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₂ :
  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₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0
⊢ { 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₁))) }
have hy₁ : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
Tactic: replace hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0 := by convert! hy using 1; ring
Cleared hypotheses: 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₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ { 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 }.b =
    { 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₁))) }.b
have pos : -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₂ =
  -(x₁ + 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₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            W.a₂ -
          x₁ -
        x₁))
Tactic: simp only [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₁ 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₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
⊢ { 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 }.c =
    { 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₁))) }.c
have pos : (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
      (x₁ * 2 * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) +
        (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (x₁ * W.a₁ - 2 * y₁ - W.a₃)) +
    HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 * (-(W.a₁ * y₁) + W.a₄) =
  x₁ *
    ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
            (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
          W.a₂ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
        x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 +
      ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
              (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
            W.a₂ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
          x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
        x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2))
Tactic: simp [field]
-- 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 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, hx
-- 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₂
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₆
⊢ { 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, 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₁ :
  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₆
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 neg : { a := 1, b := -HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
    c :=
      2 * x₁ * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
        (-W.a₁ * y₁ + W.a₄),
    d :=
      -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 +
          (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
        (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
    Cubic F } =
  { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))),
    c := x₁ * x₂ + x₁ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) + x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)),
    d := -(x₁ * x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) }
Tactic: rw [slope_of_X_ne 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₁ :
  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₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ { a := 1, b := -HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
      c :=
        2 * x₁ * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) + x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)),
      d := -(x₁ * x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) }
have neg : { a := 1, b := -HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
    c :=
      2 * x₁ * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
        (-W.a₁ * y₁ + W.a₄),
    d :=
      -HPow.hPow (β := ℕ) x₁ 2 * HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 +
          (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
        (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
    Cubic F } =
  { a := 1,
    b := -(x₁ + x₂ + (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)),
    c :=
      x₁ * x₂ + x₁ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂) +
        x₂ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂),
    d := -(x₁ * x₂ * (HPow.hPow (β := ℕ) ((y₁ - y₂) / (x₁ - x₂)) 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) }
Tactic: simp only [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
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (C : (a : F[X]) → F[X][Y]) (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) =
    -HMul.hMul (β := 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]) (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])
            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X])) :
          F[X][Y])
have rw : (C : (a : F[X]) → F[X][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]))) =
  -HMul.hMul (β := 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]) (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])
          (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) : F[X])) :
        F[X][Y])
Tactic: rw [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₂)
⊢ (derivative : (a : F[X]) → F[X]) (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]) 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]))
have rw : (derivative : (a : F[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]) 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]))
Tactic: rw [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₂)
⊢ (derivative : (a : F[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]) 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]))
have derivative_simp : -((HSub.hSub (α := F[X]) 1 0 * 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]) 1 0) *
        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]) x₂ : F[X]) *
        HSub.hSub (α := F[X]) 1 0) =
  -(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]))
Tactic: derivative_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'.Nonsingular (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
have rw : 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
Tactic: rw [Nonsingular, and_iff_right hx', negAddY, polynomialX, polynomialY]