awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
a :
  (HPow.hPow (β := ℕ) (P y) 2 * P z + W.a₁ * P x * P y * P z + W.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (HPow.hPow (β := ℕ) (P x) 3 + W.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                W.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W.a₆ * HPow.hPow (β := ℕ) (P z) 3)) /
          HPow.hPow (β := ℕ) (P z) 3 +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                W.a₃ * P y / P z * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
            W.a₄ * P x / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (HPow.hPow (β := ℕ) (P y / P z) 2 + W.toAffine.a₁ * (P x / P z) * (P y / P z) + W.toAffine.a₃ * (P y / P z) -
          (HPow.hPow (β := ℕ) (P x / P z) 3 + W.toAffine.a₂ * HPow.hPow (β := ℕ) (P x / P z) 2 +
              W.toAffine.a₄ * (P x / P z) +
            W.toAffine.a₆) +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                W.a₃ * P y / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 3) +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                W.a₃ * P y / P z * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
            W.a₄ * P x / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                W.a₃ * P y / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0

Tactic:
rw [eval_polynomial, Affine.evalEval_polynomial]

Premises used: WeierstrassCurve.Projective.eval_polynomial, WeierstrassCurve.Affine.evalEval_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (HPow.hPow (β := ℕ) (P y) 2 * P z + W.a₁ * P x * P y * P z + W.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (HPow.hPow (β := ℕ) (P x) 3 + W.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                W.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W.a₆ * HPow.hPow (β := ℕ) (P z) 3)) /
          HPow.hPow (β := ℕ) (P z) 3 +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                W.a₃ * P y / P z * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
            W.a₄ * P x / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (HPow.hPow (β := ℕ) (P y / P z) 2 + W.toAffine.a₁ * (P x / P z) * (P y / P z) + W.toAffine.a₃ * (P y / P z) -
          (HPow.hPow (β := ℕ) (P x / P z) 3 + W.toAffine.a₂ * HPow.hPow (β := ℕ) (P x / P z) 2 +
              W.toAffine.a₄ * (P x / P z) +
            W.toAffine.a₆) +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                W.a₃ * P y / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
a :
  HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 3) +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * 1 +
                W.a₃ * P y / P z * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
            W.a₄ * P x / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial +
        (HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                  W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
                W.a₃ * P y / P z * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 3) =
    Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial

Tactic:
linear_combination (norm := (rw [eval_polynomial, Affine.evalEval_polynomial]; ring1))
    P y ^ 2 / P z ^ 2 * div_self hPz + W.a₁ * P x * P y / P z ^ 2 * div_self hPz
      + W.a₃ * P y / P z * div_self (pow_ne_zero 2 hPz) - W.a₂ * P x ^ 2 / P z ^ 2 * div_self hPz
      - W.a₄ * P x / P z * div_self (pow_ne_zero 2 hPz) - W.a₆ * div_self (pow_ne_zero 3 hPz)

Premises used: WeierstrassCurve.Projective.eval_polynomial, pow_ne_zero, WeierstrassCurve.a₂, WeierstrassCurve.a₃, WeierstrassCurve.a₆, WeierstrassCurve.a₄, WeierstrassCurve.Affine.evalEval_polynomial, OfNat.ofNat, div_self, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw :
  Eq (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) (0 : R) ↔
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0
rw₁ :
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0 ↔
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0
rw₂ rw₃ :
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 =
      HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3 ↔
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 =
      HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3
⊢ W'.Equation P ↔
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
      0

Tactic:
rw [Equation, eval_polynomial, sub_eq_zero]

Premises used: WeierstrassCurve.Projective.eval_polynomial, WeierstrassCurve.Projective.Equation, sub_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P_1 : Fin 3 → R
u_1 : R
hu : IsUnit u_1
u : R
P : Fin 3 → R
hP : W'.Equation P
rw :
  ∀
    (hP :
      HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
        0),
    HPow.hPow (β := ℕ) ((u • P) y) 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
          W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
        (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
            W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 3) =
      0
⊢ W'.Equation (u • P)

Tactic:
rw [equation_iff] at hP ⊢

Premises used: WeierstrassCurve.Projective.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P_1 : Fin 3 → R
u_1 : R
hu : IsUnit u_1
u : R
P : Fin 3 → R
hP :
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
    0
a :
  HPow.hPow (β := ℕ) (u * P y) 2 * (u * P z) + W'.a₁ * (u * P x) * (u * P y) * (u * P z) +
            W'.a₃ * (u * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
          (HPow.hPow (β := ℕ) (u * P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 * (u * P z) +
              W'.a₄ * (u * P x) * HPow.hPow (β := ℕ) (u * P z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 3) +
        HPow.hPow (β := ℕ) u 3 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 3 *
          (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
    0
⊢ HPow.hPow (β := ℕ) ((u • P) y) 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
            W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
          (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
              W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 3) +
        HPow.hPow (β := ℕ) u 3 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 3 *
          (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
    0

Tactic:
simp only [smul_fin3_ext]

Premises used: WeierstrassCurve.Projective.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P_1 : Fin 3 → R
u_1 : R
hu : IsUnit u_1
u : R
P : Fin 3 → R
hP :
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
    0
⊢ HPow.hPow (β := ℕ) (u * P y) 2 * (u * P z) + W'.a₁ * (u * P x) * (u * P y) * (u * P z) +
            W'.a₃ * (u * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
          (HPow.hPow (β := ℕ) (u * P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 * (u * P z) +
              W'.a₄ * (u * P x) * HPow.hPow (β := ℕ) (u * P z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 3) +
        HPow.hPow (β := ℕ) u 3 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 3 *
          (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P_1 : Fin 3 → R
u_1 : R
hu : IsUnit u_1
u : R
P : Fin 3 → R
hP :
  HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3) =
    0
a :
  HPow.hPow (β := ℕ) ((u • P) y) 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
            W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
          (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
              W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 3) +
        HPow.hPow (β := ℕ) u 3 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 3 *
          (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
    0
⊢ HPow.hPow (β := ℕ) ((u • P) y) 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
        W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
      (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
          W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 3) =
    0

Tactic:
linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) u ^ 3 * hP

Premises used: WeierstrassCurve.Projective.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ W'.Equation ((↑hu.unit⁻¹ : R) • u • P)

Tactic:
hP (↑hu.unit⁻¹) h

Premises used: Units.val, Inv.inv, IsUnit.unit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
h₁ : P = (↑hu.unit⁻¹ : R) • u • P
⊢ W'.Equation P

Tactic:
convert! hP (↑hu.unit⁻¹) h

Premises used: Units.val, Inv.inv, IsUnit.unit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
h₁ : P = ((↑hu.unit⁻¹ : R) * u) • P
h₂ : P = HSMul.hSMul (α := R) 1 P
h₃ h₄ : P = P
⊢ P = (↑hu.unit⁻¹ : R) • u • P

Tactic:
rw [smul_smul, hu.val_inv_mul, one_smul]

Premises used: smul_smul, one_smul, IsUnit.val_inv_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
rcases : ∀ (u : Rˣ), W'.Equation ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Equation Q
⊢ W'.Equation P ↔ W'.Equation Q

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Equation Q

Tactic:
equation_smul Q u.isUnit

Premises used: WeierstrassCurve.Projective.equation_smul, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Equation Q

Tactic:
exact equation_smul Q u.isUnit

Premises used: WeierstrassCurve.Projective.equation_smul, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.Equation P ↔ HPow.hPow (β := ℕ) (P x) 3 = 0

Tactic:
simp only [equation_iff, hPz, add_zero, zero_sub, mul_zero, zero_pow <| OfNat.ofNat_ne_zero _,
    neg_eq_zero]

Premises used: OfNat.ofNat_ne_zero, neg_eq_zero, MulZeroClass.mul_zero, add_zero, WeierstrassCurve.Projective.equation_iff, zero_pow, zero_sub
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
⊢ W'.Equation ![0, 1, 0]

Tactic:
simp only [equation_of_Z_eq_zero, fin3_def_ext, zero_pow three_ne_zero]

Premises used: WeierstrassCurve.Projective.equation_of_Z_eq_zero, WeierstrassCurve.Projective.fin3_def_ext, three_ne_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
a b : R
⊢ W'.Equation ![a, b, 1] ↔ W'.toAffine.Equation a b

Tactic:
simp only [equation_iff, Affine.equation_iff', fin3_def_ext, one_pow, mul_one]

Premises used: one_pow, WeierstrassCurve.Affine.equation_iff', WeierstrassCurve.Projective.fin3_def_ext, mul_one, WeierstrassCurve.Projective.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Equation P ↔ W.toAffine.Equation (P x / P z) (P y / P z)

Tactic:
(equation_of_equiv <| equiv_some_of_Z_ne_zero hPz).trans <| equation_some ..

Premises used: WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero, Iff.trans, WeierstrassCurve.Projective.equation_of_equiv, WeierstrassCurve.Projective.equation_some
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ P x = 0

Tactic:
eq_zero_of_pow_eq_zero <| (equation_of_Z_eq_zero hPz).mp hP

Premises used: WeierstrassCurve.Projective.equation_of_Z_eq_zero, Iff.mp, eq_zero_of_pow_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw :
  (eval P : (a : MvPolynomial (Fin 3) R) → R)
      (HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) Y *
          Z -
        ((C : (a : R) → MvPolynomial (Fin 3) R) 3 * HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2 +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) (2 * W'.a₂) : MvPolynomial (Fin 3) R) X *
              Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R)
            (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2))) =
    W'.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2)
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX =
    W'.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2)

Tactic:
rw [polynomialX_eq]

Premises used: WeierstrassCurve.Projective.polynomialX_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R)
      (HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) Y *
          Z -
        ((C : (a : R) → MvPolynomial (Fin 3) R) 3 * HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2 +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) (2 * W'.a₂) : MvPolynomial (Fin 3) R) X *
              Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R)
            (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2))) =
    W'.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
a :
  (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2)) /
          HPow.hPow (β := ℕ) (P z) 2 +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) +
          W.a₄ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) -
      (W.toAffine.a₁ * (P y / P z) -
          (3 * HPow.hPow (β := ℕ) (P x / P z) 2 + 2 * W.toAffine.a₂ * (P x / P z) + W.toAffine.a₄) +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 2) +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) +
          W.a₄ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0

Tactic:
rw [eval_polynomialX, Affine.evalEval_polynomialX]

Premises used: WeierstrassCurve.Projective.eval_polynomialX, WeierstrassCurve.Affine.evalEval_polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2)) /
          HPow.hPow (β := ℕ) (P z) 2 +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) +
          W.a₄ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) -
      (W.toAffine.a₁ * (P y / P z) -
          (3 * HPow.hPow (β := ℕ) (P x / P z) 2 + 2 * W.toAffine.a₂ * (P x / P z) + W.toAffine.a₄) +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
a :
  HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 2) +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) +
          W.a₄ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 2) =
    Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX

Tactic:
linear_combination (norm := (rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1))
    W.a₁ * P y / P z * div_self hPz - 2 * W.a₂ * P x / P z * div_self hPz
      - W.a₄ * div_self (pow_ne_zero 2 hPz)

Premises used: WeierstrassCurve.Projective.eval_polynomialX, pow_ne_zero, WeierstrassCurve.a₂, WeierstrassCurve.a₄, WeierstrassCurve.Affine.evalEval_polynomialX, OfNat.ofNat, div_self, WeierstrassCurve.a₁