awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
inr : LT.lt (α := WithBot ℕ) 1 3
⊢ 1 < f.degree

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
inr : LT.lt (α := WithBot ℕ) 0 3
⊢ g.degree < f.degree

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ LT.lt (α := WithBot ℕ) 1 3

Tactic:
decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : IsDomain R
h_1 : ¬Irreducible (M := R[X][Y]) W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : degree { a := 0, b := 0, c := W.a₁, d := W.a₃ : Cubic R }.toPoly = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ LT.lt (α := WithBot ℕ) 0 3

Tactic:
decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
eval_simp :
  HPow.hPow (β := ℕ) y 2 + (W.a₁ * x + W.a₃) * y -
      (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₆)
⊢ evalEval x y
      (HSub.hSub (β := R[X][Y])
        (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
          HMul.hMul (α := R[X][Y]) (β := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W.a₃ : R[X])) :
              R[X][Y])
            Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W.a₆ : R[X])) :
          R[X][Y])) =
    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:
eval_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
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₆) =
    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₆)
rw₁ 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₆) =
    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 (β := ℕ) y 2 + (W.a₁ * x + W.a₃) * y -
      (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 [add_mul, ← add_assoc]

Premises used: add_mul, add_assoc
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
⊢ evalEval 0 0 W.polynomial = -W.a₆

Tactic:
simp only [evalEval_polynomial, zero_add, zero_sub, mul_zero, zero_pow <| Nat.succ_ne_zero _]

Premises used: zero_add, MulZeroClass.mul_zero, Nat.succ_ne_zero, WeierstrassCurve.Affine.evalEval_polynomial, zero_pow, zero_sub
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
rw :
  evalEval x y W.polynomial = 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
rw₁ 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 (β := ℕ) 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.Equation x y ↔
    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 [Equation, evalEval_polynomial]

Premises used: WeierstrassCurve.Affine.Equation, WeierstrassCurve.Affine.evalEval_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
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 (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y =
      HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆
rw₁ 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₆ ↔
    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₆
⊢ W.Equation x y ↔
    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', sub_eq_zero]

Premises used: sub_eq_zero, WeierstrassCurve.Affine.equation_iff'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
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
rw₂ rw₃ : W.a₆ = 0 ↔ W.a₆ = 0
⊢ W.Equation 0 0 ↔ W.a₆ = 0

Tactic:
rw [Equation, evalEval_polynomial_zero, neg_eq_zero]

Premises used: neg_eq_zero, WeierstrassCurve.Affine.evalEval_polynomial_zero, WeierstrassCurve.Affine.Equation
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
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
⊢ W.Equation x y ↔
    (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Equation 0
      0

Tactic:
rw [equation_iff', ← neg_eq_zero, equation_zero, variableChange_a₆, inv_one, Units.val_one]

Premises used: inv_one, WeierstrassCurve.Affine.equation_iff', neg_eq_zero, WeierstrassCurve.Affine.equation_zero, Units.val_one, WeierstrassCurve.variableChange_a₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
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₁)
⊢ -(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:
congr! 1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
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₆)) =
    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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ evalEval 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])) =
    W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)

Tactic:
eval_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
⊢ evalEval 0 0 W.polynomialX = -W.a₄

Tactic:
simp only [evalEval_polynomialX, zero_add, zero_sub, mul_zero, zero_pow <| Nat.succ_ne_zero _]

Premises used: zero_add, MulZeroClass.mul_zero, Nat.succ_ne_zero, WeierstrassCurve.Affine.evalEval_polynomialX, zero_pow, zero_sub
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
eval_simp : 2 * y + (W.a₁ * x + W.a₃) = 2 * y + W.a₁ * x + W.a₃
⊢ 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₃

Tactic:
eval_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
rw rw₁ : 2 * y + W.a₁ * x + W.a₃ = 2 * y + W.a₁ * x + W.a₃
⊢ 2 * y + (W.a₁ * x + W.a₃) = 2 * y + W.a₁ * x + W.a₃

Tactic:
rw [← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
⊢ evalEval 0 0 W.polynomialY = W.a₃

Tactic:
simp only [evalEval_polynomialY, zero_add, mul_zero]

Premises used: zero_add, MulZeroClass.mul_zero, WeierstrassCurve.Affine.evalEval_polynomialY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [Nonsingular, equation_iff', evalEval_polynomialX, evalEval_polynomialY]

Premises used: WeierstrassCurve.Affine.equation_iff', WeierstrassCurve.Affine.Nonsingular, WeierstrassCurve.Affine.evalEval_polynomialY, WeierstrassCurve.Affine.evalEval_polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
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)
⊢ 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₃)

Tactic:
rw [nonsingular_iff', sub_ne_zero, ← sub_ne_zero (a := y)]

Premises used: sub_ne_zero, WeierstrassCurve.Affine.nonsingular_iff'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
a : 2 * y + W.a₁ * x + W.a₃ = y - (-y - W.a₁ * x - W.a₃)
⊢ 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:
congr! 3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ 2 * y + W.a₁ * x + W.a₃ = y - (-y - W.a₁ * x - W.a₃)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
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)
rw₅ 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)

Tactic:
rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero,
    or_comm]

Premises used: WeierstrassCurve.Affine.equation_zero, WeierstrassCurve.Affine.Nonsingular, WeierstrassCurve.Affine.evalEval_polynomialY_zero, neg_ne_zero, or_comm, WeierstrassCurve.Affine.evalEval_polynomialX_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
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)
⊢ W.Nonsingular x y ↔
    (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Nonsingular
      0 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]

Premises used: inv_one, WeierstrassCurve.Affine.nonsingular_zero, WeierstrassCurve.Affine.equation_iff_variableChange, WeierstrassCurve.variableChange_a₃, WeierstrassCurve.Affine.equation_zero, WeierstrassCurve.variableChange_a₄, Units.val_one, neg_ne_zero, or_comm, WeierstrassCurve.Affine.nonsingular_iff'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
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)
⊢ (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:
simp only [variableChange_def]

Premises used: WeierstrassCurve.variableChange_def
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
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)
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)
⊢ 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:
congr! 3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ 2 * y + W.a₁ * x + W.a₃ = HPow.hPow (α := R) (β := ℕ) 1 3 * (W.a₃ + x * W.a₁ + 2 * y)

Tactic:
ring1