awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
a :
  P z * Q z * (P y * Q z - Q y * P z) * (P y * Q z - W'.negY Q * P z) +
        (HPow.hPow (β := ℕ) (Q z) 3 * 0 +
            HPow.hPow (β := ℕ) (P z) 3 *
              (HPow.hPow (β := ℕ) (Q y) 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 2 -
                (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * Q z +
                    W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₆ * HPow.hPow (β := ℕ) (Q z) 3)) +
          (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 + P x * Q x * P z * Q z +
                      HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                    W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₂ * P x * HPow.hPow (β := ℕ) (Q z) 2 * P z +
                W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2) *
            (Q x * P z)) -
      (0 +
        (HPow.hPow (β := ℕ) (Q 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)) +
            HPow.hPow (β := ℕ) (P z) 3 * 0 +
          (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 + P x * Q x * P z * Q z +
                      HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                    W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₂ * P x * HPow.hPow (β := ℕ) (Q z) 2 * P z +
                W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2) *
            (P x * Q z))) =
    0
⊢ P z * Q z * (P y * Q z - Q y * P z) * (P y * Q z - W'.negY Q * P z) = 0

Tactic:
linear_combination (norm := (rw [negY]; ring1)) Q z ^ 3 * (equation_iff P).mp hP
    - P z ^ 3 * (equation_iff Q).mp hQ + (P x ^ 2 * Q z ^ 2 + P x * Q x * P z * Q z
      + Q x ^ 2 * P z ^ 2 - W'.a₁ * P y * P z * Q z ^ 2 + W'.a₂ * P x * Q z ^ 2 * P z
      + W'.a₂ * Q x * P z ^ 2 * Q z + W'.a₄ * P z ^ 2 * Q z ^ 2) * hx

Premises used: WeierstrassCurve.Projective.negY, HMul.hMul, HSub.hSub, WeierstrassCurve.a₂, HPow.hPow, HAdd.hAdd, Iff.mp, WeierstrassCurve.a₄, OfNat.ofNat, WeierstrassCurve.Projective.equation_iff, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ P y * Q z = W'.negY Q * P z

Tactic:
sub_eq_zero.mp <| (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <|
    mul_ne_zero (mul_ne_zero hPz hQz) <| sub_ne_zero.mpr hy

Premises used: Iff.mpr, sub_eq_zero, sub_ne_zero, WeierstrassCurve.Projective.Y_sub_Y_mul_Y_sub_negY, Or.resolve_left, mul_eq_zero, Iff.mp, mul_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W'.negY Q * P z
⊢ P y * Q z = Q y * P z

Tactic:
sub_eq_zero.mp <| (mul_eq_zero.mp <| (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx
    ).resolve_right <| sub_ne_zero.mpr hy).resolve_left <| mul_ne_zero hPz hQz

Premises used: Iff.mpr, sub_eq_zero, sub_ne_zero, WeierstrassCurve.Projective.Y_sub_Y_mul_Y_sub_negY, Or.resolve_left, mul_eq_zero, Iff.mp, Or.resolve_right, mul_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ P y * Q z = W.negY Q * P z ↔ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z)

Tactic:
negY_of_Z_ne_zero hQz ▸ (div_eq_div_iff hPz hQz).symm

Premises used: WeierstrassCurve.Projective.negY_of_Z_ne_zero, Eq.rec, div_eq_div_iff, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
a :
  P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * Q z + -W'.a₁ * (P x * Q z)) =
    0
⊢ P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - W'.negY P) * Q z + -W'.a₁ * (P x * Q z)) =
    0

Tactic:
rw [negY, negY]

Premises used: WeierstrassCurve.Projective.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * Q z + -W'.a₁ * (P x * Q z)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
a :
  P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - W'.negY P) * Q z + -W'.a₁ * (P x * Q z)) =
    0
⊢ P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) = (P y - W'.negY P) * Q z

Tactic:
linear_combination (norm := (rw [negY, negY]; ring1)) -W'.a₁ * hx

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ P y * Q z - W'.negY Q * P z = 0

Tactic:
have hy' : P y * Q z - W'.negY Q * P z = 0 := sub_eq_zero.mpr <| Y_eq_of_Y_ne hP hQ hPz hQz hx hy
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
hy' : P y * Q z - W'.negY Q * P z = 0
contrapose : ∀ (hy : P y = W'.negY P), P y * Q z = Q y * P z
⊢ P y ≠ W'.negY P

Tactic:
contrapose hy
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - W'.negY Q * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z + ((P y - W'.negY P) * Q z + Q z * W'.negY P + (P y * Q z - W'.negY Q * P z)) -
      (Q y * P z + (P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + Q z * P y + 0)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - W'.negY Q * P z = 0
hy : P y = W'.negY P
a :
  P y * Q z + ((P y - W'.negY P) * Q z + Q z * W'.negY P + (P y * Q z - W'.negY Q * P z)) -
      (Q y * P z + (P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + Q z * P y + 0)) =
    0
⊢ P y * Q z = Q y * P z

Tactic:
linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy'

Premises used: OfNat.ofNat, WeierstrassCurve.Projective.Y_sub_Y_add_Y_sub_negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W'.negY Q * P z
⊢ P y * Q z - Q y * P z = 0

Tactic:
have hy' : P y * Q z - Q y * P z = 0 := sub_eq_zero.mpr <| Y_eq_of_Y_ne' hP hQ hPz hQz hx hy
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W'.negY Q * P z
hy' : P y * Q z - Q y * P z = 0
contrapose : ∀ (hy : P y = W'.negY P), P y * Q z = W'.negY Q * P z
⊢ P y ≠ W'.negY P

Tactic:
contrapose hy
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - Q y * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z + ((P y - W'.negY P) * Q z + Q z * W'.negY P + (P y * Q z - Q y * P z)) -
      (W'.negY Q * P z + (P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + Q z * P y + 0)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - Q y * P z = 0
hy : P y = W'.negY P
a :
  P y * Q z + ((P y - W'.negY P) * Q z + Q z * W'.negY P + (P y * Q z - Q y * P z)) -
      (W'.negY Q * P z + (P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + Q z * P y + 0)) =
    0
⊢ P y * Q z = W'.negY Q * P z

Tactic:
linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy'

Premises used: OfNat.ofNat, WeierstrassCurve.Projective.Y_sub_Y_add_Y_sub_negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ (fun (a : R) ↦ a * Q z) (P y) +
        (P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + Q y * P z + W'.negY Q * P z) -
      ((fun (a : R) ↦ a * Q z) (W'.negY P) + ((P y - W'.negY P) * Q z + P y * Q z + P y * Q z)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
a :
  (fun (a : R) ↦ a * Q z) (P y) +
        (P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + Q y * P z + W'.negY Q * P z) -
      ((fun (a : R) ↦ a * Q z) (W'.negY P) + ((P y - W'.negY P) * Q z + P y * Q z + P y * Q z)) =
    0
⊢ Eq.{r + 1} (α := R) ((fun (a : R) ↦ a * Q z) (P y)) ((fun (a : R) ↦ a * Q z) (W'.negY P))

Tactic:
linear_combination (norm := ring1) -Y_sub_Y_add_Y_sub_negY hx + hy + hy'

Premises used: WeierstrassCurve.Projective.Y_sub_Y_add_Y_sub_negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
rw :
  2 * P y * P z + W.a₁ * P x * P z + W.a₃ * HPow.hPow (β := ℕ) (P z) 2 = (P y - (-P y - W.a₁ * P x - W.a₃ * P z)) * P z
⊢ (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z

Tactic:
rw [negY, eval_polynomialY]

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.Projective.eval_polynomialY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ 2 * P y * P z + W.a₁ * P x * P z + W.a₃ * HPow.hPow (β := ℕ) (P z) 2 = (P y - (-P y - W.a₁ * P x - W.a₃ * P z)) * P z

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z

Tactic:
have hy' : eval P W.polynomialY = (P y - W.negY P) * P z := by rw [negY, eval_polynomialY]; ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
rw :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F)) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₁ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (P y - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₂ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (W.negY P - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₃ :
  W.Equation P ∧ (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ 0 * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₄ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ Ne.{u + 1} (α := F) 0 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₅ :
  W.Equation P ∧ (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ False) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₆ rw₇ :
  W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
⊢ W.Nonsingular P ↔ W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)

Tactic:
rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]

Premises used: ne_self_iff_false, sub_self, MulZeroClass.zero_mul, WeierstrassCurve.Projective.nonsingular_iff_of_Z_ne_zero, or_false
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
rw :
  HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
      HPow.hPow (β := ℕ) (P z) 2 =
    HPow.hPow (β := ℕ)
        (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))
        3 /
      HPow.hPow (β := ℕ) (P z) 2
rw₁ rw₂ :
  HPow.hPow (β := ℕ)
        (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))
        3 /
      HPow.hPow (β := ℕ) (P z) 2 =
    HPow.hPow (β := ℕ)
        (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))
        3 /
      HPow.hPow (β := ℕ) (P z) 2
⊢ W.dblU P =
    HPow.hPow (β := ℕ)
        (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))
        3 /
      HPow.hPow (β := ℕ) (P z) 2

Tactic:
rw [dblU, eval_polynomialX]

Premises used: WeierstrassCurve.Projective.dblU, WeierstrassCurve.Projective.eval_polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
u : F
⊢ W.dblU (u • P) = HPow.hPow (β := ℕ) u 4 * W.dblU P

Tactic:
simp [field, dblU_eq]

Premises used: WeierstrassCurve.Projective.dblU_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z = 0
rw :
  HPow.hPow (β := ℕ)
        (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))
        3 /
      HPow.hPow (β := ℕ) (P z) 2 =
    0
rw₁ :
  HPow.hPow (β := ℕ)
        (W.a₁ * P y * 0 -
          (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * 0 + W.a₄ * HPow.hPow (α := F) (β := ℕ) 0 2))
        3 /
      HPow.hPow (α := F) (β := ℕ) 0 2 =
    0
rw₂ : HPow.hPow (β := ℕ) (W.a₁ * P y * 0 - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * 0 + W.a₄ * 0)) 3 / 0 = 0
rw₃ rw₄ : Eq.{u + 1} (α := F) 0 0
⊢ W.dblU P = 0

Tactic:
rw [dblU_eq, hPz, zero_pow two_ne_zero, div_zero]

Premises used: WeierstrassCurve.Projective.dblU_eq, two_ne_zero, div_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.dblU P ≠ 0

Tactic:
div_ne_zero (pow_ne_zero 3
    ((nonsingular_iff_of_Y_eq_negY hPz <| Y_eq_negY_of_Y_eq hQz hx hy hy').mp hP).right) <|
    pow_ne_zero 2 hPz

Premises used: WeierstrassCurve.Projective.dblU, pow_ne_zero, WeierstrassCurve.Projective.Y_eq_negY_of_Y_eq, div_ne_zero, And.right, Iff.mp, OfNat.ofNat, WeierstrassCurve.Projective.nonsingular_iff_of_Y_eq_negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ IsUnit (W.dblU P)

Tactic:
(dblU_ne_zero_of_Y_eq hP hPz hQz hx hy hy').isUnit

Premises used: WeierstrassCurve.Projective.dblU_ne_zero_of_Y_eq, Ne.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
simp :
  u * P z * HPow.hPow (β := ℕ) (u * P y - u * W'.negY P) 3 =
    HPow.hPow (β := ℕ) u 4 * (P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3)
⊢ W'.dblZ (u • P) = HPow.hPow (β := ℕ) u 4 * W'.dblZ P

Tactic:
simp only [dblZ, negY_smul, smul_fin3_ext]

Premises used: WeierstrassCurve.Projective.negY_smul, WeierstrassCurve.Projective.smul_fin3_ext, WeierstrassCurve.Projective.dblZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ u * P z * HPow.hPow (β := ℕ) (u * P y - u * W'.negY P) 3 =
    HPow.hPow (β := ℕ) u 4 * (P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hPz : P z = 0
rw : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
rw₁ : 0 * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
rw₂ rw₃ : Eq.{r + 1} (α := R) 0 0
⊢ W'.dblZ P = 0

Tactic:
rw [dblZ, hPz, zero_mul]

Premises used: MulZeroClass.zero_mul, WeierstrassCurve.Projective.dblZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
rw : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
rw₁ : P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 = 0
rw₂ : P z * HPow.hPow (α := R) (β := ℕ) 0 3 = 0
rw₃ : P z * 0 = 0
rw₄ rw₅ : Eq.{r + 1} (α := R) 0 0
⊢ W'.dblZ P = 0

Tactic:
rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, zero_pow three_ne_zero, mul_zero]

Premises used: sub_self, WeierstrassCurve.Projective.Y_eq_negY_of_Y_eq, MulZeroClass.mul_zero, three_ne_zero, zero_pow, WeierstrassCurve.Projective.dblZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ W'.dblZ P ≠ 0

Tactic:
mul_ne_zero hPz <| pow_ne_zero 3 <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne hP hQ hPz hQz hx hy

Premises used: Iff.mpr, sub_ne_zero, pow_ne_zero, mul_ne_zero, WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne, OfNat.ofNat, WeierstrassCurve.Projective.dblZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ IsUnit (W.dblZ P)

Tactic:
(dblZ_ne_zero_of_Y_ne hP hQ hPz hQz hx hy).isUnit

Premises used: WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne, Ne.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W'.negY Q * P z
⊢ W'.dblZ P ≠ 0

Tactic:
mul_ne_zero hPz <| pow_ne_zero 3 <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy

Premises used: Iff.mpr, sub_ne_zero, pow_ne_zero, WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne', mul_ne_zero, OfNat.ofNat, WeierstrassCurve.Projective.dblZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ IsUnit (W.dblZ P)

Tactic:
(dblZ_ne_zero_of_Y_ne' hP hQ hPz hQz hx hy).isUnit

Premises used: Ne.isUnit, WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ P x / P z = Q x / Q z

Tactic:
simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy

Premises used: WeierstrassCurve.Projective.Y_eq_iff', ne_eq, WeierstrassCurve.Projective.X_eq_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
hx₁ : P x / P z = Q x / Q z
⊢ ¬P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z)

Tactic:
simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy

Premises used: WeierstrassCurve.Projective.Y_eq_iff', ne_eq, WeierstrassCurve.Projective.X_eq_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z)
rw :
  (3 * HPow.hPow (β := ℕ) (P x / P z) 2 + 2 * W.toAffine.a₂ * (P x / P z) + W.toAffine.a₄ -
        W.toAffine.a₁ * (P y / P z)) /
      (P y / P z - W.negY P / P z) =
    HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P)
⊢ W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) =
    HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P)

Tactic:
rw [Affine.slope_of_Y_ne hx <| negY_of_Z_ne_zero hQz ▸ hy, ← negY_of_Z_ne_zero hPz]

Premises used: WeierstrassCurve.Affine.slope_of_Y_ne, WeierstrassCurve.Projective.negY_of_Z_ne_zero