awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
rw : evalEval 0 0 W.polynomial = 0 ↔ W.a₆ = 0
rw₁ : -W.a₆ = 0 ↔ W.a₆ = 0
⊢ W.Equation 0 0 ↔ W.a₆ = 0
have rw₂ : W.a₆ = 0 ↔ W.a₆ = 0
Tactic: rw [Equation, evalEval_polynomial_zero, neg_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔
    (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Equation 0
      0
have rw : -(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 ↔
  HPow.hPow (α := R) (β := ℕ) 1 6 *
      (W.a₆ + VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₄ +
                HPow.hPow (β := ℕ) (VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R }) 2 * W.a₂ +
              HPow.hPow (β := ℕ) (VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R }) 3 -
            VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₃ -
          HPow.hPow (β := ℕ) (VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R }) 2 -
        VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } *
            VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R } *
          W.a₁) =
    0
Tactic: rw [equation_iff', ← neg_eq_zero, equation_zero, variableChange_a₆, inv_one, Units.val_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ -(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 ↔
    HPow.hPow (α := R) (β := ℕ) 1 6 *
        (W.a₆ + VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₄ +
                  HPow.hPow (β := ℕ) (VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R }) 2 * W.a₂ +
                HPow.hPow (β := ℕ) (VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R }) 3 -
              VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₃ -
            HPow.hPow (β := ℕ) (VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R }) 2 -
          VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } *
              VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R } *
            W.a₁) =
      0
have 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₆)) =
  HPow.hPow (α := R) (β := ℕ) 1 6 *
    (W.a₆ + VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₄ +
              HPow.hPow (β := ℕ) (VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R }) 2 * W.a₂ +
            HPow.hPow (β := ℕ) (VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R }) 3 -
          VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₃ -
        HPow.hPow (β := ℕ) (VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R }) 2 -
      VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } *
          VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R } *
        W.a₁)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ evalEval 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])) =
    2 * y + W.a₁ * x + W.a₃
have eval_simp : 2 * y + (W.a₁ * x + W.a₃) = 2 * y + W.a₁ * x + W.a₃
Tactic: eval_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ 2 * y + (W.a₁ * x + W.a₃) = 2 * y + W.a₁ * x + W.a₃
have rw : 2 * y + W.a₁ * x + W.a₃ = 2 * y + W.a₁ * x + W.a₃
Tactic: rw [← add_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular x y ↔
    W.Equation x y ∧ (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
have rw : W.Equation x y ∧ (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0) ↔
  W.Equation x y ∧ (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
Tactic: rw [Nonsingular, equation_iff', evalEval_polynomialX, evalEval_polynomialY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
rw :
  W.Equation x y ∧ (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0) ↔
    W.Equation x y ∧ (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
⊢ W.Nonsingular x y ↔
    W.Equation x y ∧ (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
have rw₁ : 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 ∧
    (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 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 ∧
    (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
Tactic: rw [Nonsingular, equation_iff', evalEval_polynomialX, evalEval_polynomialY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
rw :
  W.Equation x y ∧ (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0) ↔
    W.Equation x y ∧ (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
rw₁ :
  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 ∧
      (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 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 ∧
      (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
⊢ W.Nonsingular x y ↔
    W.Equation x y ∧ (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
have rw₂ : 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 ∧
    (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ evalEval x y W.polynomialY ≠ 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 ∧
    (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
Tactic: rw [Nonsingular, equation_iff', evalEval_polynomialX, evalEval_polynomialY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
rw :
  W.Equation x y ∧ (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0) ↔
    W.Equation x y ∧ (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
rw₁ :
  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 ∧
      (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 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 ∧
      (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
rw₂ :
  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 ∧
      (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ evalEval x y W.polynomialY ≠ 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 ∧
      (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
⊢ W.Nonsingular x y ↔
    W.Equation x y ∧ (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
have rw₃ : 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 ∧
    (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 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 ∧
    (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
Tactic: rw [Nonsingular, equation_iff', evalEval_polynomialX, evalEval_polynomialY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular 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₃)
have rw : W.Equation x y ∧ (W.a₁ * y ≠ 3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄ ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
  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₃) ≠ 0)
Tactic: rw [nonsingular_iff', sub_ne_zero, ← sub_ne_zero (a := y)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ∧ (W.a₁ * y ≠ 3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄ ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
    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₃) ≠ 0)
have a : 2 * y + W.a₁ * x + W.a₃ = y - (-y - W.a₁ * x - W.a₃)
Tactic: congr! 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
⊢ W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
have rw : W.Equation 0 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
Tactic: rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero,
    or_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
rw :
  W.Equation 0 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
⊢ W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
have rw₁ : W.a₆ = 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
Tactic: rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero,
    or_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
rw :
  W.Equation 0 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₁ : W.a₆ = 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
⊢ W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
have rw₂ : W.a₆ = 0 ∧ (-W.a₄ ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
Tactic: rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero,
    or_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
rw :
  W.Equation 0 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₁ : W.a₆ = 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₂ : W.a₆ = 0 ∧ (-W.a₄ ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
⊢ W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
have rw₃ : W.a₆ = 0 ∧ (W.a₄ ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
Tactic: rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero,
    or_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
rw :
  W.Equation 0 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₁ : W.a₆ = 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₂ : W.a₆ = 0 ∧ (-W.a₄ ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₃ : W.a₆ = 0 ∧ (W.a₄ ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
⊢ W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
have rw₄ : W.a₆ = 0 ∧ (W.a₄ ≠ 0 ∨ W.a₃ ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
Tactic: rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero,
    or_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
rw :
  W.Equation 0 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₁ : W.a₆ = 0 ∧ (evalEval 0 0 W.polynomialX ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₂ : W.a₆ = 0 ∧ (-W.a₄ ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₃ : W.a₆ = 0 ∧ (W.a₄ ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
rw₄ : W.a₆ = 0 ∧ (W.a₄ ≠ 0 ∨ W.a₃ ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
⊢ W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
have rw₅ : W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
Tactic: rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero,
    or_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular x y ↔
    (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Nonsingular
      0 0
have rw : (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).a₆ = 0 ∧
    (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
  (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).a₆ = 0 ∧
    (HPow.hPow (α := R) (β := ℕ) 1 3 *
          (W.a₃ + VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₁ +
            2 * VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R }) ≠
        0 ∨
      HPow.hPow (α := R) (β := ℕ) 1 4 *
          (W.a₄ - VariableChange.s { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₃ +
                  2 * VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₂ -
                (VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R } +
                    VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } *
                      VariableChange.s { u := 1, r := x, s := 0, t := y : VariableChange R }) *
                  W.a₁ +
              3 * HPow.hPow (β := ℕ) (VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R }) 2 -
            2 * VariableChange.s { u := 1, r := x, s := 0, t := y : VariableChange R } *
              VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R }) ≠
        0)
Tactic: rw [nonsingular_iff', equation_iff_variableChange, equation_zero, ← neg_ne_zero, or_comm,
    nonsingular_zero, variableChange_a₃, variableChange_a₄, inv_one, Units.val_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).a₆ = 0 ∧
      (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
    (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).a₆ = 0 ∧
      (HPow.hPow (α := R) (β := ℕ) 1 3 *
            (W.a₃ + VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₁ +
              2 * VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R }) ≠
          0 ∨
        HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - VariableChange.s { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₃ +
                    2 * VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } * W.a₂ -
                  (VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R } +
                      VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R } *
                        VariableChange.s { u := 1, r := x, s := 0, t := y : VariableChange R }) *
                    W.a₁ +
                3 * HPow.hPow (β := ℕ) (VariableChange.r { u := 1, r := x, s := 0, t := y : VariableChange R }) 2 -
              2 * VariableChange.s { u := 1, r := x, s := 0, t := y : VariableChange R } *
                VariableChange.t { u := 1, r := x, s := 0, t := y : VariableChange R }) ≠
          0)
have simp : HPow.hPow (α := R) (β := ℕ) (↑1⁻¹ : R) 6 *
        (W.a₆ + x * W.a₄ + HPow.hPow (β := ℕ) x 2 * W.a₂ + HPow.hPow (β := ℕ) x 3 - y * W.a₃ - HPow.hPow (β := ℕ) y 2 -
          x * y * W.a₁) =
      0 ∧
    (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
  HPow.hPow (α := R) (β := ℕ) (↑1⁻¹ : R) 6 *
        (W.a₆ + x * W.a₄ + HPow.hPow (β := ℕ) x 2 * W.a₂ + HPow.hPow (β := ℕ) x 3 - y * W.a₃ - HPow.hPow (β := ℕ) y 2 -
          x * y * W.a₁) =
      0 ∧
    (HPow.hPow (α := R) (β := ℕ) 1 3 * (W.a₃ + x * W.a₁ + 2 * y) ≠ 0 ∨
      HPow.hPow (α := R) (β := ℕ) 1 4 *
          (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * HPow.hPow (β := ℕ) x 2 -
            HMul.hMul (α := R) 2 0 * y) ≠
        0)
Tactic: simp only [variableChange_def]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ HPow.hPow (α := R) (β := ℕ) (↑1⁻¹ : R) 6 *
          (W.a₆ + x * W.a₄ + HPow.hPow (β := ℕ) x 2 * W.a₂ + HPow.hPow (β := ℕ) x 3 - y * W.a₃ -
              HPow.hPow (β := ℕ) y 2 -
            x * y * W.a₁) =
        0 ∧
      (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
    HPow.hPow (α := R) (β := ℕ) (↑1⁻¹ : R) 6 *
          (W.a₆ + x * W.a₄ + HPow.hPow (β := ℕ) x 2 * W.a₂ + HPow.hPow (β := ℕ) x 3 - y * W.a₃ -
              HPow.hPow (β := ℕ) y 2 -
            x * y * W.a₁) =
        0 ∧
      (HPow.hPow (α := R) (β := ℕ) 1 3 * (W.a₃ + x * W.a₁ + 2 * y) ≠ 0 ∨
        HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * HPow.hPow (β := ℕ) x 2 -
              HMul.hMul (α := R) 2 0 * y) ≠
          0)
have a : 2 * y + W.a₁ * x + W.a₃ = HPow.hPow (α := R) (β := ℕ) 1 3 * (W.a₃ + x * W.a₁ + 2 * y)
Tactic: congr! 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
a : 2 * y + W.a₁ * x + W.a₃ = HPow.hPow (α := R) (β := ℕ) 1 3 * (W.a₃ + x * W.a₁ + 2 * y)
⊢ HPow.hPow (α := R) (β := ℕ) (↑1⁻¹ : R) 6 *
          (W.a₆ + x * W.a₄ + HPow.hPow (β := ℕ) x 2 * W.a₂ + HPow.hPow (β := ℕ) x 3 - y * W.a₃ -
              HPow.hPow (β := ℕ) y 2 -
            x * y * W.a₁) =
        0 ∧
      (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
    HPow.hPow (α := R) (β := ℕ) (↑1⁻¹ : R) 6 *
          (W.a₆ + x * W.a₄ + HPow.hPow (β := ℕ) x 2 * W.a₂ + HPow.hPow (β := ℕ) x 3 - y * W.a₃ -
              HPow.hPow (β := ℕ) y 2 -
            x * y * W.a₁) =
        0 ∧
      (HPow.hPow (α := R) (β := ℕ) 1 3 * (W.a₃ + x * W.a₁ + 2 * y) ≠ 0 ∨
        HPow.hPow (α := R) (β := ℕ) 1 4 *
            (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * HPow.hPow (β := ℕ) x 2 -
              HMul.hMul (α := R) 2 0 * y) ≠
          0)
have a₁ : -(W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)) =
  HPow.hPow (α := R) (β := ℕ) 1 4 *
    (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * HPow.hPow (β := ℕ) x 2 - HMul.hMul (α := R) 2 0 * y)
Tactic: congr! 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
hΔ : Δ W ≠ 0
⊢ W.Equation 0 0 ↔ W.Nonsingular 0 0
have simp : W.a₆ = 0 → W.a₃ ≠ 0 ∨ W.a₄ ≠ 0
Tactic: simp only [equation_zero, nonsingular_zero, iff_self_and]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
hΔ : Δ W ≠ 0
⊢ W.a₆ = 0 → W.a₃ ≠ 0 ∨ W.a₄ ≠ 0
have contrapose! : ∀ (hΔ : W.a₆ = 0 ∧ W.a₃ = 0 ∧ W.a₄ = 0), Δ W = 0
Tactic: contrapose! hΔ
Cleared hypotheses: hΔ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
hΔ : W.a₆ = 0 ∧ W.a₃ = 0 ∧ W.a₄ = 0
⊢ Δ W = 0
have simp : -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) 2 *
          (HPow.hPow (β := ℕ) W.a₁ 2 * 0 + 4 * W.a₂ * 0 - W.a₁ * 0 * 0 + W.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 -
            HPow.hPow (α := R) (β := ℕ) 0 2) -
        8 * HPow.hPow (β := ℕ) (HMul.hMul (α := R) 2 0 + W.a₁ * 0) 3 -
      27 * HPow.hPow (β := ℕ) (HPow.hPow (α := R) (β := ℕ) 0 2 + HMul.hMul (α := R) 4 0) 2 +
    9 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) * (HMul.hMul (α := R) 2 0 + W.a₁ * 0) *
      (HPow.hPow (α := R) (β := ℕ) 0 2 + HMul.hMul (α := R) 4 0) =
  0
Tactic: simp only [b₂, b₄, b₆, b₈, Δ, hΔ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
⊢ Δ (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)) ≠ 0
have rwa : HPow.hPow (β := ℕ) (↑(VariableChange.u { u := 1, r := x, s := 0, t := y : VariableChange R })⁻¹ : R) 12 * Δ W ≠ 0
Tactic: rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
rwa : HPow.hPow (β := ℕ) (↑(VariableChange.u { u := 1, r := x, s := 0, t := y : VariableChange R })⁻¹ : R) 12 * Δ W ≠ 0
⊢ Δ (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)) ≠ 0
have rwa₁ : HPow.hPow (α := R) (β := ℕ) (↑1 : R) 12 * Δ W ≠ 0
Tactic: rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]