awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 2) +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) +
          W.a₄ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0
have a : (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)) /
        HPow.hPow (β := ℕ) (P z) 2 +
      (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) +
        W.a₄ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) -
    (W.toAffine.a₁ * (P y / P z) -
        (3 * HPow.hPow (β := ℕ) (P x / P z) 2 + 2 * W.toAffine.a₂ * (P x / P z) + W.toAffine.a₄) +
      (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
  0
Tactic: rw [eval_polynomialX, Affine.evalEval_polynomialX]
-- 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
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 2) =
    Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX
have a : HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 2) +
      (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) +
        W.a₄ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2)) -
    (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX +
      (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
  0
Tactic: linear_combination (norm := (rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1))
    W.a₁ * P y / P z * div_self hPz - 2 * W.a₂ * P x / P z * div_self hPz
      - W.a₄ * div_self (pow_ne_zero 2 hPz)
-- 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
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY =
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2
have rw : (eval P : (a : MvPolynomial (Fin 3) R) → R)
    (HMul.hMul (α := MvPolynomial (Fin 3) R) ((C : (a : R) → MvPolynomial (Fin 3) R) 2) Y * Z +
        HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
          Z +
      HMul.hMul (α := MvPolynomial (Fin 3) R) ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R)
        (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2)) =
  2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2
Tactic: rw [polynomialY_eq]
-- 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
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (HPow.hPow (β := ℕ) (P z) 2) +
        (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY +
        (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) +
          W.a₃ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2))) =
    0
have a : (2 * P y * P z + W.a₁ * P x * P z + W.a₃ * HPow.hPow (β := ℕ) (P z) 2) / HPow.hPow (β := ℕ) (P z) 2 +
      (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
    (2 * (P y / P z) + W.toAffine.a₁ * (P x / P z) + W.toAffine.a₃ +
      (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) +
        W.a₃ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2))) =
  0
Tactic: rw [eval_polynomialY, Affine.evalEval_polynomialY]
-- 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
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (HPow.hPow (β := ℕ) (P z) 2) =
    Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY
have a : HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (HPow.hPow (β := ℕ) (P z) 2) +
      (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
    (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY +
      (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) +
        W.a₃ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2))) =
  0
Tactic: linear_combination (norm := (rw [eval_polynomialY, Affine.evalEval_polynomialY]; ring1))
    2 * P y / P z * div_self hPz + W.a₁ * P x / P z * div_self hPz
      + W.a₃ * div_self (pow_ne_zero 2 hPz)
-- 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
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ =
    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)
have rw : (eval P : (a : MvPolynomial (Fin 3) R) → R)
    (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Y 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
            Y +
        HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) (2 * W'.a₃) : MvPolynomial (Fin 3) R) Y *
          Z -
      (HMul.hMul (α := MvPolynomial (Fin 3) R) ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₂ : MvPolynomial (Fin 3) R)
            (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2) +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) (2 * W'.a₄) : MvPolynomial (Fin 3) R) X *
            Z +
        HMul.hMul (α := MvPolynomial (Fin 3) R)
          ((C : (a : R) → MvPolynomial (Fin 3) R) (3 * W'.a₆) : MvPolynomial (Fin 3) R)
          (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 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)
Tactic: rw [polynomialZ_eq]
-- 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
⊢ HMul.hMul (α := R) (β := R) (3 : R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) =
    HMul.hMul (β := R) (P x) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) +
        HMul.hMul (β := R) (P y) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY : R) +
      HMul.hMul (β := R) (P z) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R)
have rw : 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)) =
  P x *
        (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)) +
      P y * (2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2) +
    P z *
      (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))
Tactic: rw [eval_polynomial, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
-- 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
⊢ W'.Nonsingular P ↔
    W'.Equation P ∧
      (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)
have rw : W'.Equation P ∧
    (Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) (0 : R) ∨
      Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY : R) (0 : R) ∨
        Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R) (0 : R)) ↔
  W'.Equation P ∧
    (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)
Tactic: rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
-- 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
rw :
  W'.Equation P ∧
      (Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) (0 : R) ∨
        Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY : R) (0 : R) ∨
          Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R) (0 : R)) ↔
    W'.Equation P ∧
      (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'.Nonsingular P ↔
    W'.Equation P ∧
      (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)
have rw₁ : W'.Equation P ∧
    (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 ∨
      Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY : R) (0 : R) ∨
        Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R) (0 : R)) ↔
  W'.Equation P ∧
    (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)
Tactic: rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
-- 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
rw :
  W'.Equation P ∧
      (Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) (0 : R) ∨
        Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY : R) (0 : R) ∨
          Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R) (0 : R)) ↔
    W'.Equation P ∧
      (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)
rw₁ :
  W'.Equation P ∧
      (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 ∨
        Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY : R) (0 : R) ∨
          Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R) (0 : R)) ↔
    W'.Equation P ∧
      (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'.Nonsingular P ↔
    W'.Equation P ∧
      (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)
have rw₂ : W'.Equation P ∧
    (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 ∨
        Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R) (0 : R)) ↔
  W'.Equation P ∧
    (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)
Tactic: rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (hypothesis)
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 : W'.Nonsingular (u • P)
⊢ W'.Nonsingular P
have hP₁ : W'.Equation (u • P)
Tactic: rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (hypothesis)
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 : W'.Nonsingular (u • P)
hP₁ : W'.Equation (u • P)
⊢ W'.Nonsingular P
have hP' : 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: rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩
-- 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₁ * (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
⊢ W'.Nonsingular P
have refine : 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
Tactic: refine (nonsingular_iff P).mpr ⟨(equation_smul P hu).mp hP, ?_⟩
-- 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₁ * (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
⊢ 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
have contrapose! : ∀
  (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: contrapose! hP'
Cleared hypotheses: hP'
-- 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
⊢ 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
have simp : 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: simp only [smul_fin3_ext]
-- 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
⊢ 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
have a : 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) +
      HPow.hPow (β := ℕ) u 2 * 0 -
    (0 +
      HPow.hPow (β := ℕ) u 2 *
        (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
Tactic: linear_combination (norm := ring1) u ^ 2 * hP'.left
-- 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
⊢ 2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 2 = 0
have a : 2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 2 +
      HPow.hPow (β := ℕ) u 2 * 0 -
    (0 + HPow.hPow (β := ℕ) u 2 * (2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2)) =
  0
Tactic: linear_combination (norm := ring1) u ^ 2 * hP'.right.left