awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3 = 0
contrapose : ∀ (hy : P y = W'.negY P), P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
⊢ P y ≠ W'.negY P

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

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

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

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

Tactic:
have hy' : P y * Q z ^ 3 - Q y * P z ^ 3 = 0 :=
    (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_right <| sub_ne_zero_of_ne hy
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 = 0
contrapose : ∀ (hy : P y = W'.negY P), P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ P y ≠ W'.negY P

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

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

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

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

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

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

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

Tactic:
rw [negY, eval_polynomialY]

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

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian 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

Tactic:
have hy' : eval P W.polynomialY = P y - W.negY P := by rw [negY, eval_polynomialY]; ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian 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
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 ≠ 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 ≠ 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, ne_self_iff_false, or_false]

Premises used: ne_self_iff_false, sub_self, or_false, WeierstrassCurve.Jacobian.nonsingular_iff_of_Z_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
rw :
  (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 * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (P z) 4)
rw₁ rw₂ :
  W'.a₁ * P y * P z -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (P z) 4) =
    W'.a₁ * P y * P z -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (P z) 4)
⊢ W'.dblU P =
    W'.a₁ * P y * P z -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (P z) 4)

Tactic:
rw [dblU, eval_polynomialX]

Premises used: WeierstrassCurve.Jacobian.dblU, WeierstrassCurve.Jacobian.eval_polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
simp :
  W'.a₁ * (HPow.hPow (β := ℕ) u 3 * P y) * (u * P z) -
      (3 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 +
          2 * W'.a₂ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 4) =
    HPow.hPow (β := ℕ) u 4 *
      (W'.a₁ * P y * P z -
        (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₄ * HPow.hPow (β := ℕ) (P z) 4))
⊢ W'.dblU (u • P) = HPow.hPow (β := ℕ) u 4 * W'.dblU P

Tactic:
simp only [dblU_eq, smul_fin3_ext]

Premises used: WeierstrassCurve.Jacobian.dblU_eq, WeierstrassCurve.Jacobian.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.a₁ * (HPow.hPow (β := ℕ) u 3 * P y) * (u * P z) -
      (3 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 +
          2 * W'.a₂ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 4) =
    HPow.hPow (β := ℕ) u 4 *
      (W'.a₁ * P y * P z -
        (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₄ * HPow.hPow (β := ℕ) (P z) 4))

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw :
  W'.a₁ * P y * 0 -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (α := R) (β := ℕ) 0 2 +
        W'.a₄ * HPow.hPow (α := R) (β := ℕ) 0 4) =
    -3 * HPow.hPow (β := ℕ) (P x) 2
⊢ W'.dblU P = -3 * HPow.hPow (β := ℕ) (P x) 2

Tactic:
rw [dblU_eq, hPz]

Premises used: WeierstrassCurve.Jacobian.dblU_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.a₁ * P y * 0 -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (α := R) (β := ℕ) 0 2 +
        W'.a₄ * HPow.hPow (α := R) (β := ℕ) 0 4) =
    -3 * HPow.hPow (β := ℕ) (P x) 2

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ W.dblU P ≠ 0

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

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

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

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

Tactic:
simp only [dblZ, negY_smul, smul_fin3_ext]

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

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : P z * (P y - W'.negY P) = 0
rw₁ : 0 * (P y - W'.negY P) = 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.Jacobian.dblZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw : P z * (P y - W'.negY P) = 0
rw₁ : P z * (W'.negY P - W'.negY P) = 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, mul_zero]

Premises used: sub_self, WeierstrassCurve.Jacobian.dblZ, MulZeroClass.mul_zero, WeierstrassCurve.Jacobian.Y_eq_negY_of_Y_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ Q y * HPow.hPow (β := ℕ) (P z) 3
⊢ W'.dblZ P ≠ 0

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

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

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

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

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

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

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

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

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

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

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

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

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

Premises used: WeierstrassCurve.Jacobian.negY_of_Z_ne_zero, WeierstrassCurve.Affine.slope_of_Y_ne, WeierstrassCurve.Jacobian.dblZ, WeierstrassCurve.Jacobian.dblU_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x / HPow.hPow (β := ℕ) (P z) 2 = Q x / HPow.hPow (β := ℕ) (Q z) 2
hy :
  ¬P y / HPow.hPow (β := ℕ) (P z) 3 =
      W.toAffine.negY (Q x / HPow.hPow (β := ℕ) (Q z) 2) (Q y / HPow.hPow (β := ℕ) (Q z) 3)
⊢ (3 * HPow.hPow (β := ℕ) (P x / HPow.hPow (β := ℕ) (P z) 2) 2 +
            2 * W.toAffine.a₂ * (P x / HPow.hPow (β := ℕ) (P z) 2) +
          W.toAffine.a₄ -
        W.toAffine.a₁ * (P y / HPow.hPow (β := ℕ) (P z) 3)) /
      (P y / HPow.hPow (β := ℕ) (P z) 3 - W.negY P / HPow.hPow (β := ℕ) (P z) 3) =
    -(W.a₁ * P y * P z -
          (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
            W.a₄ * HPow.hPow (β := ℕ) (P z) 4)) /
      (P z * (P y - W.negY P))

Tactic:
simp [field]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
simp :
  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4 * W'.dblU P) 2 -
          W'.a₁ * (HPow.hPow (β := ℕ) u 4 * W'.dblU P) * (u * P z) *
            (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) -
        W'.a₂ * HPow.hPow (β := ℕ) (u * P z) 2 *
          HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) 2 -
      2 * (HPow.hPow (β := ℕ) u 2 * P x) *
        HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 *
      (HPow.hPow (β := ℕ) (W'.dblU P) 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) -
          W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
        2 * P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2)
⊢ W'.dblX (u • P) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P

Tactic:
simp only [dblX, dblU_smul, negY_smul, smul_fin3_ext]

Premises used: WeierstrassCurve.Jacobian.dblX, WeierstrassCurve.Jacobian.dblU_smul, WeierstrassCurve.Jacobian.negY_smul, WeierstrassCurve.Jacobian.smul_fin3_ext