awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : -P y - W'.a₁ * P x - W'.a₃ * P z = -P y
⊢ W'.negY P = -P y
have rw₁ : -P y - W'.a₁ * P x - W'.a₃ * 0 = -P y
Tactic: rw [negY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, mul_zero, sub_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : -P y - W'.a₁ * P x - W'.a₃ * P z = -P y
rw₁ : -P y - W'.a₁ * P x - W'.a₃ * 0 = -P y
⊢ W'.negY P = -P y
have rw₂ : -P y - W'.a₁ * 0 - W'.a₃ * 0 = -P y
Tactic: rw [negY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, mul_zero, sub_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : -P y - W'.a₁ * P x - W'.a₃ * P z = -P y
rw₁ : -P y - W'.a₁ * P x - W'.a₃ * 0 = -P y
rw₂ : -P y - W'.a₁ * 0 - W'.a₃ * 0 = -P y
⊢ W'.negY P = -P y
have rw₃ : -P y - 0 - W'.a₃ * 0 = -P y
Tactic: rw [negY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, mul_zero, sub_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : -P y - W'.a₁ * P x - W'.a₃ * P z = -P y
rw₁ : -P y - W'.a₁ * P x - W'.a₃ * 0 = -P y
rw₂ : -P y - W'.a₁ * 0 - W'.a₃ * 0 = -P y
rw₃ : -P y - 0 - W'.a₃ * 0 = -P y
⊢ W'.negY P = -P y
have rw₄ : -P y - W'.a₃ * 0 = -P y
Tactic: rw [negY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, mul_zero, sub_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : -P y - W'.a₁ * P x - W'.a₃ * P z = -P y
rw₁ : -P y - W'.a₁ * P x - W'.a₃ * 0 = -P y
rw₂ : -P y - W'.a₁ * 0 - W'.a₃ * 0 = -P y
rw₃ : -P y - 0 - W'.a₃ * 0 = -P y
rw₄ : -P y - W'.a₃ * 0 = -P y
⊢ W'.negY P = -P y
have rw₅ : -P y - 0 = -P y
Tactic: rw [negY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, mul_zero, sub_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : -P y - W'.a₁ * P x - W'.a₃ * P z = -P y
rw₁ : -P y - W'.a₁ * P x - W'.a₃ * 0 = -P y
rw₂ : -P y - W'.a₁ * 0 - W'.a₃ * 0 = -P y
rw₃ : -P y - 0 - W'.a₃ * 0 = -P y
rw₄ : -P y - W'.a₃ * 0 = -P y
rw₅ : -P y - 0 = -P y
⊢ W'.negY P = -P y
have rw₆ : -P y = -P y
Tactic: rw [negY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, mul_zero, sub_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / P z + -W.a₃ * 1 - (W.toAffine.negY (P x / P z) (P y / P z) + -W.a₃ * (P z / P z)) = 0
have a : (-P y - W.a₁ * P x - W.a₃ * P z) / P z + -W.a₃ * 1 -
    (-(P y / P z) - W.toAffine.a₁ * (P x / P z) - W.toAffine.a₃ + -W.a₃ * (P z / P z)) =
  0
Tactic: rw [negY, Affine.negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / P z = W.toAffine.negY (P x / P z) (P y / P z)
have a : W.negY P / P z + -W.a₃ * 1 - (W.toAffine.negY (P x / P z) (P y / P z) + -W.a₃ * (P z / P z)) = 0
Tactic: linear_combination (norm := (rw [negY, Affine.negY]; ring1)) -W.a₃ * div_self hPz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ P z * Q z * (P y * Q z - Q y * P z) * (P y * Q z - W'.negY Q * P z) = 0
have a : P z * Q z * (P y * Q z - Q y * P z) * (P y * Q z - W'.negY Q * P z) +
      (HPow.hPow (β := ℕ) (Q z) 3 * 0 +
          HPow.hPow (β := ℕ) (P z) 3 *
            (HPow.hPow (β := ℕ) (Q y) 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 2 -
              (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * Q z +
                  W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 2 +
                W'.a₆ * HPow.hPow (β := ℕ) (Q z) 3)) +
        (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 + P x * Q x * P z * Q z +
                    HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                  W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 +
                W'.a₂ * P x * HPow.hPow (β := ℕ) (Q z) 2 * P z +
              W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z +
            W'.a₄ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2) *
          (Q x * P z)) -
    (0 +
      (HPow.hPow (β := ℕ) (Q z) 3 *
            (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
              (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                  W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₆ * HPow.hPow (β := ℕ) (P z) 3)) +
          HPow.hPow (β := ℕ) (P z) 3 * 0 +
        (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 + P x * Q x * P z * Q z +
                    HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                  W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 +
                W'.a₂ * P x * HPow.hPow (β := ℕ) (Q z) 2 * P z +
              W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z +
            W'.a₄ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2) *
          (P x * Q z))) =
  0
Tactic: linear_combination (norm := (rw [negY]; ring1)) Q z ^ 3 * (equation_iff P).mp hP
    - P z ^ 3 * (equation_iff Q).mp hQ + (P x ^ 2 * Q z ^ 2 + P x * Q x * P z * Q z
      + Q x ^ 2 * P z ^ 2 - W'.a₁ * P y * P z * Q z ^ 2 + W'.a₂ * P x * Q z ^ 2 * P z
      + W'.a₂ * Q x * P z ^ 2 * Q z + W'.a₄ * P z ^ 2 * Q z ^ 2) * hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - W'.negY P) * Q z + -W'.a₁ * (P x * Q z)) =
    0
have a : P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
    ((P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * Q z + -W'.a₁ * (P x * Q z)) =
  0
Tactic: rw [negY, negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) = (P y - W'.negY P) * Q z
have a : P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + -W'.a₁ * (Q x * P z) -
    ((P y - W'.negY P) * Q z + -W'.a₁ * (P x * Q z)) =
  0
Tactic: linear_combination (norm := (rw [negY, negY]; ring1)) -W'.a₁ * hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ P y ≠ W'.negY P
have hy' : P y * Q z - W'.negY Q * P z = 0
Tactic: have hy' : P y * Q z - W'.negY Q * P z = 0 := sub_eq_zero.mpr <| Y_eq_of_Y_ne hP hQ hPz hQz hx hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
hy' : P y * Q z - W'.negY Q * P z = 0
⊢ P y ≠ W'.negY P
have contrapose : ∀ (hy : P y = W'.negY P), P y * Q z = Q y * P z
Tactic: contrapose hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - W'.negY Q * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z = Q y * P z
have a : P y * Q z + ((P y - W'.negY P) * Q z + Q z * W'.negY P + (P y * Q z - W'.negY Q * P z)) -
    (Q y * P z + (P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + Q z * P y + 0)) =
  0
Tactic: linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W'.negY Q * P z
⊢ P y ≠ W'.negY P
have hy' : P y * Q z - Q y * P z = 0
Tactic: have hy' : P y * Q z - Q y * P z = 0 := sub_eq_zero.mpr <| Y_eq_of_Y_ne' hP hQ hPz hQz hx hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W'.negY Q * P z
hy' : P y * Q z - Q y * P z = 0
⊢ P y ≠ W'.negY P
have contrapose : ∀ (hy : P y = W'.negY P), P y * Q z = W'.negY Q * P z
Tactic: contrapose hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - Q y * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z = W'.negY Q * P z
have a : P y * Q z + ((P y - W'.negY P) * Q z + Q z * W'.negY P + (P y * Q z - Q y * P z)) -
    (W'.negY Q * P z + (P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + Q z * P y + 0)) =
  0
Tactic: linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ Eq.{r + 1} (α := R) ((fun (a : R) ↦ a * Q z) (P y)) ((fun (a : R) ↦ a * Q z) (W'.negY P))
have a : (fun (a : R) ↦ a * Q z) (P y) + (P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + Q y * P z + W'.negY Q * P z) -
    ((fun (a : R) ↦ a * Q z) (W'.negY P) + ((P y - W'.negY P) * Q z + P y * Q z + P y * Q z)) =
  0
Tactic: linear_combination (norm := ring1) -Y_sub_Y_add_Y_sub_negY hx + hy + hy'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
have rw : 2 * P y * P z + W.a₁ * P x * P z + W.a₃ * HPow.hPow (β := ℕ) (P z) 2 = (P y - (-P y - W.a₁ * P x - W.a₃ * P z)) * P z
Tactic: rw [negY, eval_polynomialY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (hypothesis)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ W.Nonsingular P ↔ W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
have hy' : (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
Tactic: have hy' : eval P W.polynomialY = (P y - W.negY P) * P z := by rw [negY, eval_polynomialY]; ring1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
⊢ W.Nonsingular P ↔ W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
have 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)
Tactic: rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
rw :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F)) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
⊢ W.Nonsingular P ↔ W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
have rw₁ : W.Equation P ∧
    (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ (P y - W.negY P) * P z ≠ 0) ↔
  W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
Tactic: rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
rw :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F)) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₁ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (P y - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
⊢ W.Nonsingular P ↔ W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
have rw₂ : W.Equation P ∧
    (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
      (W.negY P - W.negY P) * P z ≠ 0) ↔
  W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
Tactic: rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
rw :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F)) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₁ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (P y - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₂ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (W.negY P - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
⊢ W.Nonsingular P ↔ W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
have rw₃ : W.Equation P ∧ (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ 0 * P z ≠ 0) ↔
  W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
Tactic: rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
rw :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F)) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₁ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (P y - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₂ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (W.negY P - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₃ :
  W.Equation P ∧ (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ 0 * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
⊢ W.Nonsingular P ↔ W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
have 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)
Tactic: rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
rw :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F)) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₁ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (P y - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₂ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (W.negY P - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₃ :
  W.Equation P ∧ (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ 0 * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₄ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ Ne.{u + 1} (α := F) 0 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
⊢ W.Nonsingular P ↔ W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
have 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)
Tactic: rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY = (P y - W.negY P) * P z
rw :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F)) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₁ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (P y - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₂ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        (W.negY P - W.negY P) * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₃ :
  W.Equation P ∧ (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ 0 * P z ≠ 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₄ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ Ne.{u + 1} (α := F) 0 0) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
rw₅ :
  W.Equation P ∧ (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨ False) ↔
    W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
⊢ W.Nonsingular P ↔ W.Equation P ∧ Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F)
have 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)
Tactic: rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
⊢ W.dblU P =
    HPow.hPow (β := ℕ)
        (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
        3 /
      HPow.hPow (β := ℕ) (P z) 2
have rw : HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
    HPow.hPow (β := ℕ) (P z) 2 =
  HPow.hPow (β := ℕ)
      (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
      3 /
    HPow.hPow (β := ℕ) (P z) 2
Tactic: rw [dblU, eval_polynomialX]