awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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 * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) =
      0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) =
        0
a :
  HPow.hPow (β := ℕ) (u * P y) 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
          (W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₄ * (u * P x) * (u * P z) +
            3 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 2) +
        HPow.hPow (β := ℕ) u 2 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 2 *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
            (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2))) =
    0
⊢ HPow.hPow (β := ℕ) (u * P y) 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
      (W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₄ * (u * P x) * (u * P z) +
        3 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 2) =
    0

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

Premises used: And.right
-- 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_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 * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) =
      0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) =
        0
⊢ W'.a₁ * (u * P y) * (u * P z) -
        (3 * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₂ * (u * P x) * (u * P z) +
          W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 2) =
      0 ∧
    2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (u * P y) 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
          (W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₄ * (u * P x) * (u * P z) +
            3 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 2) =
        0

Tactic:
exact ⟨by linear_combination (norm := ring1) u ^ 2 * hP'.left,
      by linear_combination (norm := ring1) u ^ 2 * hP'.right.left,
      by linear_combination (norm := ring1) u ^ 2 * hP'.right.right⟩
-- 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} (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.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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: Units.isUnit, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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: Units.isUnit, WeierstrassCurve.Projective.nonsingular_smul
-- 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'.Nonsingular P ↔
    W'.Equation P ∧
      (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨
        HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y - W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 ≠ 0)

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

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

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

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

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

Tactic:
linear_combination (norm := ring1) h.right

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

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

Premises used: one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 →
        HPow.hPow (β := ℕ) b 2 + W'.a₁ * a * b + 2 * W'.a₃ * b -
            (W'.a₂ * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₄ * a + 3 * 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', WeierstrassCurve.Projective.nonsingular_iff, iff_self_and, and_congr_right_iff, WeierstrassCurve.Projective.fin3_def_ext, not_and_or, Iff.comm, mul_one, WeierstrassCurve.Affine.nonsingular_iff', WeierstrassCurve.Projective.equation_some
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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
⊢ HPow.hPow (β := ℕ) b 2 + W'.a₁ * a * b + 2 * W'.a₃ * b -
          (W'.a₂ * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₄ * a + 3 * W'.a₆) +
        (HMul.hMul (α := R) 3 0 + a * (W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄)) +
          b * (2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃)) -
      (0 +
        (3 *
              (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₆)) +
            a * 0 +
          b * 0)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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₁ :
  HPow.hPow (β := ℕ) b 2 + W'.a₁ * a * b + 2 * W'.a₃ * b -
          (W'.a₂ * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₄ * a + 3 * W'.a₆) +
        (HMul.hMul (α := R) 3 0 + a * (W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄)) +
          b * (2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃)) -
      (0 +
        (3 *
              (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₆)) +
            a * 0 +
          b * 0)) =
    0
⊢ HPow.hPow (β := ℕ) b 2 + W'.a₁ * a * b + 2 * W'.a₃ * b -
      (W'.a₂ * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₄ * a + 3 * W'.a₆) =
    0

Tactic:
linear_combination (norm := ring1) 3 * h - a * ha - b * hb
-- 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.Nonsingular P ↔ W.toAffine.Nonsingular (P x / P z) (P y / P z)

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

Premises used: WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero, WeierstrassCurve.Projective.nonsingular_of_equiv, Iff.trans, WeierstrassCurve.Projective.nonsingular_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'.Nonsingular P
hPz : P z = 0
hPy : P y = 0
⊢ False

Tactic:
simp only [nonsingular_of_Z_eq_zero hPz, X_eq_zero_of_Z_eq_zero hP.left hPz, hPy, add_zero,
    sub_zero, mul_zero, zero_pow two_ne_zero, or_self, ne_self_iff_false, and_false] at hP

Premises used: ne_self_iff_false, sub_zero, MulZeroClass.mul_zero, two_ne_zero, And.left, or_self, and_false, WeierstrassCurve.Projective.nonsingular_of_Z_eq_zero, WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero, add_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective 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: Ne.isUnit, WeierstrassCurve.Projective.Y_ne_zero_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
h : (fun (m : Fˣ) ↦ m • Q) (⋯.unit / ⋯.unit) = P
⊢ P ≈ Q

Tactic:
use (isUnit_Y_of_Z_eq_zero hP hPz).unit / (isUnit_Y_of_Z_eq_zero hQ hQz).unit

Premises used: WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, IsUnit.unit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
h : ![0, P y, 0] = P
⊢ (fun (m : Fˣ) ↦ m • Q) (⋯.unit / ⋯.unit) = P

Tactic:
simp only [Units.smul_def, smul_fin3, X_eq_zero_of_Z_eq_zero hQ.left hQz, hQz, mul_zero,
    Units.val_div_eq_div_val, IsUnit.unit_spec, (isUnit_Y_of_Z_eq_zero hQ hQz).div_mul_cancel]

Premises used: WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, Units.val_div_eq_div_val, MulZeroClass.mul_zero, WeierstrassCurve.Projective.smul_fin3, And.left, Units.smul_def, WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero, IsUnit.div_mul_cancel, IsUnit.unit_spec
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
rw : ![0, P y, 0]
| P

Tactic:
rw [← fin3_def P, X_eq_zero_of_Z_eq_zero hP.left hPz, hPz]

Premises used: WeierstrassCurve.Projective.fin3_def, And.left, WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
conv_rhs : ![0, P y, 0] = P
h : ![0, P y, 0] = ![0, P y, 0]
⊢ ![0, P y, 0] = P

Tactic:
conv_rhs => rw [← fin3_def P, X_eq_zero_of_Z_eq_zero hP.left hPz, hPz]

Premises used: WeierstrassCurve.Projective.fin3_def, And.left, WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ P ≈ ![0, 1, 0]

Tactic:
equiv_of_Z_eq_zero hP nonsingular_zero hPz rfl

Premises used: WeierstrassCurve.Projective.equiv_of_Z_eq_zero, WeierstrassCurve.Projective.nonsingular_zero, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) ↔ P ≈ Q

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
refine_1 :
  ∀ (h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)), P ≈ Q
refine_2 :
  ∀ (h : P ≈ Q), HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) ↔ P ≈ Q

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
pos : ∀ (hz : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)), P ≈ Q
neg : ∀ (hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)), P ≈ Q
⊢ P ≈ Q

Tactic:
by_cases hz : f (P z) = 0

Premises used: OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ P ≈ Q

Tactic:
equiv_of_Z_eq_zero hP hQ ((map_eq_zero_iff f f.injective).mp hz) <|
        (map_eq_zero_iff f f.injective).mp <| (Z_eq_zero_of_equiv h).mp hz

Premises used: WeierstrassCurve.Projective.equiv_of_Z_eq_zero, RingHom.injective, map_eq_zero_iff, WeierstrassCurve.Projective.Z_eq_zero_of_equiv, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ P ≈ Q

Tactic:
exact equiv_of_Z_eq_zero hP hQ ((map_eq_zero_iff f f.injective).mp hz) <|
        (map_eq_zero_iff f f.injective).mp <| (Z_eq_zero_of_equiv h).mp hz

Premises used: WeierstrassCurve.Projective.equiv_of_Z_eq_zero, RingHom.injective, map_eq_zero_iff, WeierstrassCurve.Projective.Z_eq_zero_of_equiv, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ P ≈ Q

Tactic:
equiv_of_X_eq_of_Y_eq ((map_ne_zero_iff f f.injective).mp hz)
        ((map_ne_zero_iff f f.injective).mp <| hz.comp (Z_eq_zero_of_equiv h).mpr) ?_ ?_

Premises used: Iff.mpr, Function.comp, RingHom.injective, WeierstrassCurve.Projective.Z_eq_zero_of_equiv, Iff.mp, WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq, map_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg : P x * Q z = Q x * P z
neg₁ : P y * Q z = Q y * P z
⊢ P ≈ Q

Tactic:
refine equiv_of_X_eq_of_Y_eq ((map_ne_zero_iff f f.injective).mp hz)
        ((map_ne_zero_iff f f.injective).mp <| hz.comp (Z_eq_zero_of_equiv h).mpr) ?_ ?_

Premises used: Iff.mpr, Function.comp, RingHom.injective, WeierstrassCurve.Projective.Z_eq_zero_of_equiv, Iff.mp, WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq, map_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P x * Q z) : K) ((f : (a : F) → K) (Q x * P z) : K)
⊢ P x * Q z = Q x * P z

Tactic:
apply f.injective

Premises used: RingHom.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg :
  HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (P x) : K) ((f : (a : F) → K) (Q z) : K) =
    HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (Q x) : K) ((f : (a : F) → K) (P z) : K)
⊢ Eq.{v + 1} (α := K) ((f : (a : F) → K) (P x * Q z) : K) ((f : (a : F) → K) (Q x * P z) : K)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P y * Q z) : K) ((f : (a : F) → K) (Q y * P z) : K)
⊢ P y * Q z = Q y * P z

Tactic:
apply f.injective

Premises used: RingHom.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
neg :
  HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (P y) : K) ((f : (a : F) → K) (Q z) : K) =
    HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (Q y) : K) ((f : (a : F) → K) (P z) : K)
⊢ Eq.{v + 1} (α := K) ((f : (a : F) → K) (P y * Q z) : K) ((f : (a : F) → K) (Q y * P z) : K)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (P x) : K) ((f : (a : F) → K) (Q z) : K) =
    HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (Q x) : K) ((f : (a : F) → K) (P z) : K)

Tactic:
X_eq_of_equiv h

Premises used: WeierstrassCurve.Projective.X_eq_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (P y) : K) ((f : (a : F) → K) (Q z) : K) =
    HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (Q y) : K) ((f : (a : F) → K) (P z) : K)

Tactic:
Y_eq_of_equiv h

Premises used: WeierstrassCurve.Projective.Y_eq_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (P x) : K) ((f : (a : F) → K) (Q z) : K) =
    HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (Q x) : K) ((f : (a : F) → K) (P z) : K)

Tactic:
exacts [X_eq_of_equiv h, Y_eq_of_equiv h]

Premises used: WeierstrassCurve.Projective.X_eq_of_equiv, WeierstrassCurve.Projective.Y_eq_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
refine_2 :
  ∀ (u : Fˣ) (hP : W.Nonsingular ((fun (m : Fˣ) ↦ m • Q) u)),
    HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K)
      (Function.comp.{1, u + 1, v + 1} (β := F) (⇑f : (a : F) → K) ((fun (m : Fˣ) ↦ m • Q) u)) ((⇑f : (a : F) → K) ∘ Q)
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl