awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
      (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) =
    (P y - W'.negY P) * HPow.hPow (β := ℕ) (Q z) 3
have a : P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
        (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) +
      -W'.a₁ * P z * Q z * (Q x * HPow.hPow (β := ℕ) (P z) 2) -
    ((P y - W'.negY P) * HPow.hPow (β := ℕ) (Q z) 3 + -W'.a₁ * P z * Q z * (P x * HPow.hPow (β := ℕ) (Q z) 2)) =
  0
Tactic: linear_combination (norm := (rw [negY, negY]; ring1)) -W'.a₁ * P z * Q z * hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ Q y * HPow.hPow (β := ℕ) (P z) 3
⊢ P y ≠ W'.negY P
have hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3 = 0
Tactic: have hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0 :=
    (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <| sub_ne_zero_of_ne hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3 = 0
⊢ P y ≠ W'.negY P
have contrapose : ∀ (hy : P y = W'.negY P), P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
Tactic: contrapose hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3 = 0
hy : P y = W'.negY P
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
have a : P y * HPow.hPow (β := ℕ) (Q z) 3 +
      ((P y - W'.negY P) * HPow.hPow (β := ℕ) (Q z) 3 + HPow.hPow (β := ℕ) (Q z) 3 * W'.negY P +
        (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3)) -
    (Q y * HPow.hPow (β := ℕ) (P z) 3 +
      (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
            (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) +
          HPow.hPow (β := ℕ) (Q z) 3 * P y +
        0)) =
  0
Tactic: linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z ^ 3 * hy - hy'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ P y ≠ W'.negY P
have hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 = 0
Tactic: have hy' : P y * Q z ^ 3 - Q y * P z ^ 3 = 0 :=
    (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_right <| sub_ne_zero_of_ne hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 = 0
⊢ P y ≠ W'.negY P
have contrapose : ∀ (hy : P y = W'.negY P), P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
Tactic: contrapose hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 = 0
hy : P y = W'.negY P
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
have a : P y * HPow.hPow (β := ℕ) (Q z) 3 +
      ((P y - W'.negY P) * HPow.hPow (β := ℕ) (Q z) 3 + HPow.hPow (β := ℕ) (Q z) 3 * W'.negY P +
        (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) -
    (W'.negY Q * HPow.hPow (β := ℕ) (P z) 3 +
      (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
            (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) +
          HPow.hPow (β := ℕ) (Q z) 3 * P y +
        0)) =
  0
Tactic: linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z ^ 3 * hy - hy'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ Eq.{r + 1} (α := R) ((fun (a : R) ↦ a * HPow.hPow (β := ℕ) (Q z) 3) (P y))
    ((fun (a : R) ↦ a * HPow.hPow (β := ℕ) (Q z) 3) (W'.negY P))
have a : (fun (a : R) ↦ a * HPow.hPow (β := ℕ) (Q z) 3) (P y) +
      (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
            (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) +
          Q y * HPow.hPow (β := ℕ) (P z) 3 +
        W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) -
    ((fun (a : R) ↦ a * HPow.hPow (β := ℕ) (Q z) 3) (W'.negY P) +
      ((P y - W'.negY P) * HPow.hPow (β := ℕ) (Q z) 3 + P y * HPow.hPow (β := ℕ) (Q z) 3 +
        P y * HPow.hPow (β := ℕ) (Q z) 3)) =
  0
Tactic: linear_combination (norm := ring1) -Y_sub_Y_add_Y_sub_negY hx + hy + hy'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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
have rw : 2 * P y + W.a₁ * P x * P z + W.a₃ * HPow.hPow (β := ℕ) (P z) 3 =
  P y - (-P y - W.a₁ * P x * P z - W.a₃ * HPow.hPow (β := ℕ) (P z) 3)
Tactic: rw [negY, eval_polynomialY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian 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
Tactic: have hy' : eval P W.polynomialY = P y - W.negY P := by rw [negY, eval_polynomialY]; ring1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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
⊢ 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, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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
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 ≠ 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, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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
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 ≠ 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 ≠ 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, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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
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 ≠ 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 ≠ 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, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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
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 ≠ 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 ≠ 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, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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
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 ≠ 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 ≠ 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, ne_self_iff_false, or_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.dblU P =
    W'.a₁ * P y * P z -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (P z) 4)
have rw : (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX =
  W'.a₁ * P y * P z -
    (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 + W'.a₄ * HPow.hPow (β := ℕ) (P z) 4)
Tactic: rw [dblU, eval_polynomialX]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
rw :
  (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX =
    W'.a₁ * P y * P z -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (P z) 4)
⊢ W'.dblU P =
    W'.a₁ * P y * P z -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (P z) 4)
have rw₁ : W'.a₁ * P y * P z -
    (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
      W'.a₄ * HPow.hPow (β := ℕ) (P z) 4) =
  W'.a₁ * P y * P z -
    (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 + W'.a₄ * HPow.hPow (β := ℕ) (P z) 4)
Tactic: rw [dblU, eval_polynomialX]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblU (u • P) = HPow.hPow (β := ℕ) u 4 * W'.dblU P
have simp : W'.a₁ * (HPow.hPow (β := ℕ) u 3 * P y) * (u * P z) -
    (3 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 +
        2 * W'.a₂ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 2 +
      W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 4) =
  HPow.hPow (β := ℕ) u 4 *
    (W'.a₁ * P y * P z -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (P z) 4))
Tactic: simp only [dblU_eq, smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.dblU P = -3 * HPow.hPow (β := ℕ) (P x) 2
have rw : W'.a₁ * P y * 0 -
    (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (α := R) (β := ℕ) 0 2 +
      W'.a₄ * HPow.hPow (α := R) (β := ℕ) 0 4) =
  -3 * HPow.hPow (β := ℕ) (P x) 2
Tactic: rw [dblU_eq, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblZ (u • P) = HPow.hPow (β := ℕ) u 4 * W'.dblZ P
have simp : u * P z * (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) =
  HPow.hPow (β := ℕ) u 4 * (P z * (P y - W'.negY P))
Tactic: simp only [dblZ, negY_smul, smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.dblZ P = 0
have rw : P z * (P y - W'.negY P) = 0
Tactic: rw [dblZ, hPz, zero_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : P z * (P y - W'.negY P) = 0
⊢ W'.dblZ P = 0
have rw₁ : 0 * (P y - W'.negY P) = 0
Tactic: rw [dblZ, hPz, zero_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : P z * (P y - W'.negY P) = 0
rw₁ : 0 * (P y - W'.negY P) = 0
⊢ W'.dblZ P = 0
have rw₂ : Eq.{r + 1} (α := R) 0 0
Tactic: rw [dblZ, hPz, zero_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ W'.dblZ P = 0
have rw : P z * (P y - W'.negY P) = 0
Tactic: rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw : P z * (P y - W'.negY P) = 0
⊢ W'.dblZ P = 0
have rw₁ : P z * (W'.negY P - W'.negY P) = 0
Tactic: rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw : P z * (P y - W'.negY P) = 0
rw₁ : P z * (W'.negY P - W'.negY P) = 0
⊢ W'.dblZ P = 0
have rw₂ : P z * 0 = 0
Tactic: rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw : P z * (P y - W'.negY P) = 0
rw₁ : P z * (W'.negY P - W'.negY P) = 0
rw₂ : P z * 0 = 0
⊢ W'.dblZ P = 0
have rw₃ : Eq.{r + 1} (α := R) 0 0
Tactic: rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3) =
    -W.dblU P / W.dblZ P
have hx₁ : P x / HPow.hPow (β := ℕ) (P z) 2 = Q x / HPow.hPow (β := ℕ) (Q z) 2
Tactic: simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
hx₁ : P x / HPow.hPow (β := ℕ) (P z) 2 = Q x / HPow.hPow (β := ℕ) (Q z) 2
⊢ W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3) =
    -W.dblU P / W.dblZ P
have hy₁ : ¬P y / HPow.hPow (β := ℕ) (P z) 3 =
    W.toAffine.negY (Q x / HPow.hPow (β := ℕ) (Q z) 2) (Q y / HPow.hPow (β := ℕ) (Q z) 3)
Tactic: simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy
Cleared hypotheses: hx, hy