awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  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) =
      0 ∧
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = 0 ∧
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5) =
        0
⊢ 2 * (HPow.hPow (β := ℕ) u 3 * P y) + W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) +
          W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 +
        HPow.hPow (β := ℕ) u 3 * 0 -
      (0 + HPow.hPow (β := ℕ) u 3 * (2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  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) =
      0 ∧
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = 0 ∧
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5) =
        0
a :
  2 * (HPow.hPow (β := ℕ) u 3 * P y) + W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) +
          W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 +
        HPow.hPow (β := ℕ) u 3 * 0 -
      (0 + HPow.hPow (β := ℕ) u 3 * (2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) =
    0
⊢ 2 * (HPow.hPow (β := ℕ) u 3 * P y) + W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) +
      W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 =
    0

Tactic:
linear_combination (norm := ring1) u ^ 3 * hP'.right.left

Premises used: And.right, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  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) =
      0 ∧
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = 0 ∧
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5) =
        0
⊢ W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) +
            3 * W'.a₃ * (HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 * (u * P z) +
              4 * W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 5) +
        HPow.hPow (β := ℕ) u 5 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 5 *
          (W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
              6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5))) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  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) =
      0 ∧
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = 0 ∧
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5) =
        0
a :
  W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) +
            3 * W'.a₃ * (HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 * (u * P z) +
              4 * W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 5) +
        HPow.hPow (β := ℕ) u 5 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 5 *
          (W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
              6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5))) =
    0
⊢ W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) +
        3 * W'.a₃ * (HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
      (2 * W'.a₂ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 * (u * P z) +
          4 * W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 3 +
        6 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 5) =
    0

Tactic:
linear_combination (norm := ring1) u ^ 5 * hP'.right.right

Premises used: And.right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  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) =
      0 ∧
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = 0 ∧
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5) =
        0
⊢ 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) =
      0 ∧
    2 * (HPow.hPow (β := ℕ) u 3 * P y) + W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) +
          W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 =
        0 ∧
      W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) +
            3 * W'.a₃ * (HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 * (u * P z) +
              4 * W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 5) =
        0

Tactic:
exact ⟨by linear_combination (norm := ring1) u ^ 4 * hP'.left,
      by linear_combination (norm := ring1) u ^ 3 * hP'.right.left,
      by linear_combination (norm := ring1) u ^ 5 * hP'.right.right⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ {u : R} (hu : IsUnit u) {P : Fin 3 → R} (hP : W'.Nonsingular (u • P)), W'.Nonsingular P
h : W'.Nonsingular P
rwa : W'.Nonsingular (((↑hu.unit⁻¹ : R) * u) • P)
rwa₁ : W'.Nonsingular (HSMul.hSMul (α := R) 1 P)
rwa₂ rwa₃ rwa₄ rwa₅ : W'.Nonsingular P
⊢ W'.Nonsingular ((↑hu.unit⁻¹ : R) • u • P)

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

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

Tactic:
rcases h with ⟨u, rfl⟩

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

Tactic:
nonsingular_smul Q u.isUnit

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

Tactic:
exact nonsingular_smul Q u.isUnit

Premises used: WeierstrassCurve.Jacobian.nonsingular_smul, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.Nonsingular P ↔ W'.Equation P ∧ (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0)

Tactic:
simp only [nonsingular_iff, hPz, add_zero, sub_zero, zero_sub, mul_zero,
    zero_pow <| OfNat.ofNat_ne_zero _, neg_ne_zero]

Premises used: OfNat.ofNat_ne_zero, sub_zero, MulZeroClass.mul_zero, neg_ne_zero, add_zero, WeierstrassCurve.Jacobian.nonsingular_iff, zero_pow, zero_sub
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : Nontrivial R
simp : ¬(3 * HPow.hPow (α := R) (β := ℕ) 1 2 = 0 ∧ HMul.hMul (α := R) 2 1 = 0 ∧ W'.a₁ * 1 * 1 = 0)
⊢ W'.Nonsingular ![1, 1, 0]

Tactic:
simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]

Premises used: WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero, WeierstrassCurve.Jacobian.fin3_def_ext, not_and_or, WeierstrassCurve.Jacobian.equation_zero, true_and
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : Nontrivial R
h : 3 * HPow.hPow (α := R) (β := ℕ) 1 2 = 0 ∧ HMul.hMul (α := R) 2 1 = 0 ∧ W'.a₁ * 1 * 1 = 0
⊢ 1 + (0 + HMul.hMul (α := R) 2 1) - (0 + (3 * HPow.hPow (α := R) (β := ℕ) 1 2 + 0)) = 0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : Nontrivial R
h : 3 * HPow.hPow (α := R) (β := ℕ) 1 2 = 0 ∧ HMul.hMul (α := R) 2 1 = 0 ∧ W'.a₁ * 1 * 1 = 0
a : 1 + (0 + HMul.hMul (α := R) 2 1) - (0 + (3 * HPow.hPow (α := R) (β := ℕ) 1 2 + 0)) = 0
⊢ Eq.{r + 1} (α := R) 1 0

Tactic:
linear_combination (norm := ring1) h.1 - h.2.1

Premises used: And.right, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : Nontrivial R
⊢ ¬(3 * HPow.hPow (α := R) (β := ℕ) 1 2 = 0 ∧ HMul.hMul (α := R) 2 1 = 0 ∧ W'.a₁ * 1 * 1 = 0)

Tactic:
exact fun h => one_ne_zero <| by linear_combination (norm := ring1) h.1 - h.2.1

Premises used: one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
a b : R
simp_rw :
  HPow.hPow (β := ℕ) b 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (HPow.hPow (β := ℕ) a 3 + W'.toAffine.a₂ * HPow.hPow (β := ℕ) a 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
      2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0 →
        W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * HPow.hPow (β := ℕ) a 2 + 4 * W'.a₄ * a + 6 * W'.a₆) = 0
⊢ W'.Nonsingular ![a, b, 1] ↔ W'.toAffine.Nonsingular a b

Tactic:
simp_rw [nonsingular_iff, equation_some, fin3_def_ext, Affine.nonsingular_iff',
    Affine.equation_iff', and_congr_right_iff, ← not_and_or, not_iff_not, one_pow, mul_one,
    and_congr_right_iff, Iff.comm, iff_self_and]

Premises used: not_iff_not, one_pow, WeierstrassCurve.Affine.equation_iff', iff_self_and, and_congr_right_iff, WeierstrassCurve.Jacobian.fin3_def_ext, not_and_or, Iff.comm, WeierstrassCurve.Jacobian.equation_some, mul_one, WeierstrassCurve.Affine.nonsingular_iff', WeierstrassCurve.Jacobian.nonsingular_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
a b : R
h :
  HPow.hPow (β := ℕ) b 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
      (HPow.hPow (β := ℕ) a 3 + W'.toAffine.a₂ * HPow.hPow (β := ℕ) a 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
    0
ha : W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄) = 0
hb : 2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0
⊢ W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * HPow.hPow (β := ℕ) a 2 + 4 * W'.a₄ * a + 6 * W'.a₆) +
        (HMul.hMul (α := R) 6 0 + 2 * a * (W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄)) +
          3 * b * (2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃)) -
      (0 +
        (6 *
              (HPow.hPow (β := ℕ) b 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
                (HPow.hPow (β := ℕ) a 3 + W'.toAffine.a₂ * HPow.hPow (β := ℕ) a 2 + W'.toAffine.a₄ * a +
                  W'.toAffine.a₆)) +
            2 * a * 0 +
          3 * b * 0)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
a b : R
h :
  HPow.hPow (β := ℕ) b 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
      (HPow.hPow (β := ℕ) a 3 + W'.toAffine.a₂ * HPow.hPow (β := ℕ) a 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
    0
ha : W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄) = 0
hb : 2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0
a₁ :
  W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * HPow.hPow (β := ℕ) a 2 + 4 * W'.a₄ * a + 6 * W'.a₆) +
        (HMul.hMul (α := R) 6 0 + 2 * a * (W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄)) +
          3 * b * (2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃)) -
      (0 +
        (6 *
              (HPow.hPow (β := ℕ) b 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
                (HPow.hPow (β := ℕ) a 3 + W'.toAffine.a₂ * HPow.hPow (β := ℕ) a 2 + W'.toAffine.a₄ * a +
                  W'.toAffine.a₆)) +
            2 * a * 0 +
          3 * b * 0)) =
    0
⊢ W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * HPow.hPow (β := ℕ) a 2 + 4 * W'.a₄ * a + 6 * W'.a₆) = 0

Tactic:
linear_combination (norm := ring1) 6 * h - 2 * a * ha - 3 * b * hb
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Nonsingular P ↔ W.toAffine.Nonsingular (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)

Tactic:
(nonsingular_of_equiv <| equiv_some_of_Z_ne_zero hPz).trans <| nonsingular_some ..

Premises used: WeierstrassCurve.Jacobian.nonsingular_some, Iff.trans, WeierstrassCurve.Jacobian.nonsingular_of_equiv, WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x = 0
⊢ HPow.hPow (β := ℕ) (P y) 2 = 0 ∧ 2 * P y ≠ 0

Tactic:
simp only [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPx, mul_zero, zero_mul,
    zero_pow <| OfNat.ofNat_ne_zero _, ne_self_iff_false, or_false, false_or] at hP

Premises used: ne_self_iff_false, OfNat.ofNat_ne_zero, MulZeroClass.zero_mul, WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero, false_or, MulZeroClass.mul_zero, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero, or_false, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : HPow.hPow (β := ℕ) (P y) 2 = 0 ∧ 2 * P y ≠ 0
rwa : ∀ (hP : P y = 0 ∧ 2 * P y ≠ 0), False
rwa₁ : ∀ (hP : Eq.{r + 1} (α := R) 0 0 ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
rwa₂ : ∀ (hP : True ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
rwa₃ : ∀ (hP : HMul.hMul (α := R) 2 0 ≠ 0), False
rwa₄ : ∀ (hP : Ne.{r + 1} (α := R) 0 0), False
rwa₅ rwa₆ rwa₇ rwa₈ : ∀ (hP : False), False
⊢ False

Tactic:
rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP

Premises used: ne_self_iff_false, pow_eq_zero_iff, MulZeroClass.mul_zero, two_ne_zero, And.left, eq_self, true_and
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ IsUnit (P x)

Tactic:
(X_ne_zero_of_Z_eq_zero hP hPz).isUnit

Premises used: WeierstrassCurve.Jacobian.X_ne_zero_of_Z_eq_zero, Ne.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P x ≠ 0

Tactic:
have hPx : P x ≠ 0 := X_ne_zero_of_Z_eq_zero hP hPz
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ 0 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ HMul.hMul (α := R) 2 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)

Tactic:
rw [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPy, zero_pow two_ne_zero] at hP

Premises used: WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero, two_ne_zero, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
hP₁ :
  0 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ HMul.hMul (α := R) 2 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
⊢ P z = 0

Tactic:
rw [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPy, zero_pow two_ne_zero] at hP

Premises used: WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero, two_ne_zero, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
hP₁ :
  0 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ HMul.hMul (α := R) 2 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
hPz₁ : P z = 0
⊢ P x ≠ 0

Tactic:
rw [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPy, zero_pow two_ne_zero] at hP

Premises used: WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero, two_ne_zero, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
hP₁ :
  0 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ HMul.hMul (α := R) 2 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
hPz₁ : P z = 0
hPx₁ : P x ≠ 0
⊢ P y = 0

Tactic:
rw [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPy, zero_pow two_ne_zero] at hP

Premises used: WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero, two_ne_zero, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP :
  0 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ HMul.hMul (α := R) 2 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Tactic:
hPx <| eq_zero_of_pow_eq_zero hP.left.symm

Premises used: And.left, eq_zero_of_pow_eq_zero, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP :
  0 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ HMul.hMul (α := R) 2 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Tactic:
exact hPx <| eq_zero_of_pow_eq_zero hP.left.symm

Premises used: And.left, eq_zero_of_pow_eq_zero, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ IsUnit (P y)

Tactic:
(Y_ne_zero_of_Z_eq_zero hP hPz).isUnit

Premises used: WeierstrassCurve.Jacobian.Y_ne_zero_of_Z_eq_zero, Ne.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ IsUnit (P x)

Tactic:
have hPx : IsUnit <| P x := isUnit_X_of_Z_eq_zero hP hPz
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
⊢ IsUnit (P y)

Tactic:
have hPy : IsUnit <| P y := isUnit_Y_of_Z_eq_zero hP hPz
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
⊢ IsUnit (Q x)

Tactic:
have hQx : IsUnit <| Q x := isUnit_X_of_Z_eq_zero hQ hQz
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
⊢ IsUnit (Q y)

Tactic:
have hQy : IsUnit <| Q y := isUnit_Y_of_Z_eq_zero hQ hQz
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
⊢ HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)

Tactic:
simp only [nonsingular_of_Z_eq_zero, equation_of_Z_eq_zero, hPz, hQz] at hP hQ

Premises used: WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP₁ :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
⊢ HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)

Tactic:
simp only [nonsingular_of_Z_eq_zero, equation_of_Z_eq_zero, hPz, hQz] at hP hQ

Premises used: WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h : (fun (m : Fˣ) ↦ m • Q) (hPy.unit / hPx.unit * (hQx.unit / hQy.unit)) = P
⊢ P ≈ Q

Tactic:
use (hPy.unit / hPx.unit) * (hQx.unit / hQy.unit)

Premises used: HDiv.hDiv, IsUnit.unit