awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ 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
have 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
Tactic: linear_combination (norm := ring1) u ^ 2 * hP'.right.right
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ W'.Nonsingular ((↑hu.unit⁻¹ : R) • u • P)
have rwa : W'.Nonsingular (((↑hu.unit⁻¹ : R) * u) • P)
Tactic: rwa [smul_smul, hu.val_inv_mul, one_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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)
⊢ W'.Nonsingular ((↑hu.unit⁻¹ : R) • u • P)
have rwa₁ : W'.Nonsingular (HSMul.hSMul (α := R) 1 P)
Tactic: rwa [smul_smul, hu.val_inv_mul, one_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Nonsingular P ↔ W'.Nonsingular Q
have rcases : ∀ (u : Rˣ), W'.Nonsingular ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Nonsingular Q
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : Nontrivial R
⊢ W'.Nonsingular ![0, 1, 0]
have 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)
Tactic: simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ Eq.{r + 1} (α := R) 1 0
have a : HAdd.hAdd (α := R) 1 0 -
    (0 + (HPow.hPow (α := R) (β := ℕ) 1 2 + W'.a₁ * 0 * 1 - W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2)) =
  0
Tactic: linear_combination (norm := ring1) h.right
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
a b : R
⊢ W'.Nonsingular ![a, b, 1] ↔ W'.toAffine.Nonsingular a b
have 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
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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₆) =
    0
have 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
Tactic: linear_combination (norm := ring1) 3 * h - a * ha - b * hb
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Nonsingular P ↔
    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))
have rw : W.toAffine.Nonsingular (P x / P z) (P y / P z) ↔
  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))
Tactic: rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
    ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz,
    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  W.toAffine.Nonsingular (P x / P z) (P y / P z) ↔
    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.Nonsingular P ↔
    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))
have rw₁ : W.toAffine.Equation (P x / P z) (P y / P z) ∧
    (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX ≠ 0 ∨
      Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
  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))
Tactic: rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
    ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz,
    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  W.toAffine.Nonsingular (P x / P z) (P y / P z) ↔
    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))
rw₁ :
  W.toAffine.Equation (P x / P z) (P y / P z) ∧
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX ≠ 0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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.Nonsingular P ↔
    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))
have rw₂ : W.Equation P ∧
    (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX ≠ 0 ∨
      Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
  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))
Tactic: rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
    ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz,
    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  W.toAffine.Nonsingular (P x / P z) (P y / P z) ↔
    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))
rw₁ :
  W.toAffine.Equation (P x / P z) (P y / P z) ∧
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX ≠ 0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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))
rw₂ :
  W.Equation P ∧
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX ≠ 0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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.Nonsingular P ↔
    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))
have rw₃ : W.Equation P ∧
    (HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 2) ≠
        0 ∨
      Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
  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))
Tactic: rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
    ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz,
    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  W.toAffine.Nonsingular (P x / P z) (P y / P z) ↔
    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))
rw₁ :
  W.toAffine.Equation (P x / P z) (P y / P z) ∧
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX ≠ 0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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))
rw₂ :
  W.Equation P ∧
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX ≠ 0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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))
rw₃ :
  W.Equation P ∧
      (HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 2) ≠
          0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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.Nonsingular P ↔
    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))
have rw₄ : W.Equation P ∧
    (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∧
        HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
      Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
  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))
Tactic: rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
    ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz,
    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  W.toAffine.Nonsingular (P x / P z) (P y / P z) ↔
    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))
rw₁ :
  W.toAffine.Equation (P x / P z) (P y / P z) ∧
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX ≠ 0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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))
rw₂ :
  W.Equation P ∧
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX ≠ 0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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))
rw₃ :
  W.Equation P ∧
      (HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 2) ≠
          0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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))
rw₄ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∧
          HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    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.Nonsingular P ↔
    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))
have rw₅ : W.Equation P ∧
    (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
      Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
  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))
Tactic: rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
    ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz,
    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ P ≈ Q
have h : (fun (m : Fˣ) ↦ m • Q) (sorry.unit / sorry.unit) = P
Tactic: use (isUnit_Y_of_Z_eq_zero hP hPz).unit / (isUnit_Y_of_Z_eq_zero hQ hQz).unit
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ (fun (m : Fˣ) ↦ m • Q) (⋯.unit / ⋯.unit) = P
have h : ![0, P y, 0] = 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
| P
have rw : ![0, P y, 0]
Tactic: rw [← fin3_def P, X_eq_zero_of_Z_eq_zero hP.left hPz, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ ![0, P y, 0] = P
have conv_rhs : ![0, P y, 0] = P
Tactic: conv_rhs => rw [← fin3_def P, X_eq_zero_of_Z_eq_zero hP.left hPz, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ ![0, P y, 0] = P
have h : ![0, P y, 0] = ![0, P y, 0]
Tactic: conv_rhs => rw [← fin3_def P, X_eq_zero_of_Z_eq_zero hP.left hPz, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
have 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
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) ↔ P ≈ Q
have 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)
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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)
⊢ P ≈ Q
have pos : ∀ (hz : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)), P ≈ Q
Tactic: by_cases hz : f (P z) = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ P ≈ Q
have neg : ∀ (hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)), P ≈ Q
Tactic: by_cases hz : f (P z) = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
have neg : P x * Q z = Q x * P z
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) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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
⊢ P ≈ Q
have neg₁ : P y * Q z = Q y * P z
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) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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 x * Q z = Q x * P z
have neg : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P x * Q z) : K) ((f : (a : F) → K) (Q x * P z) : K)
Tactic: apply f.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
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)
⊢ Eq.{v + 1} (α := K) ((f : (a : F) → K) (P x * Q z) : K) ((f : (a : F) → K) (Q x * P z) : K)
have 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)
Tactic: map_simp