awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  W.toAffine.Nonsingular (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ↔
    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 / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ∧
      (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            W.toAffine.polynomialX ≠
          0 ∨
        Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            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 / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            W.toAffine.polynomialX ≠
          0 ∨
        Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            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) 4) ≠
          0 ∨
        Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            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) 4 ≠ 0 ∨
      Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) 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 4 hPz,
    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 3 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x = 0
⊢ False
have hP₁ : HPow.hPow (β := ℕ) (P y) 2 = 0 ∧ 2 * P y ≠ 0
Tactic: simp only [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPx, mul_zero, zero_mul,
    zero_pow <| OfNat.ofNat_ne_zero _, ne_self_iff_false, or_false, false_or] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : HPow.hPow (β := ℕ) (P y) 2 = 0 ∧ 2 * P y ≠ 0
⊢ False
have rwa : ∀ (hP : P y = 0 ∧ 2 * P y ≠ 0), False
Tactic: rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : HPow.hPow (β := ℕ) (P y) 2 = 0 ∧ 2 * P y ≠ 0
rwa : ∀ (hP : P y = 0 ∧ 2 * P y ≠ 0), False
⊢ False
have rwa₁ : ∀ (hP : Eq.{r + 1} (α := R) 0 0 ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
Tactic: rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : HPow.hPow (β := ℕ) (P y) 2 = 0 ∧ 2 * P y ≠ 0
rwa : ∀ (hP : P y = 0 ∧ 2 * P y ≠ 0), False
rwa₁ : ∀ (hP : Eq.{r + 1} (α := R) 0 0 ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
⊢ False
have rwa₂ : ∀ (hP : True ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
Tactic: rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : HPow.hPow (β := ℕ) (P y) 2 = 0 ∧ 2 * P y ≠ 0
rwa : ∀ (hP : P y = 0 ∧ 2 * P y ≠ 0), False
rwa₁ : ∀ (hP : Eq.{r + 1} (α := R) 0 0 ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
rwa₂ : ∀ (hP : True ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
⊢ False
have rwa₃ : ∀ (hP : HMul.hMul (α := R) 2 0 ≠ 0), False
Tactic: rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : HPow.hPow (β := ℕ) (P y) 2 = 0 ∧ 2 * P y ≠ 0
rwa : ∀ (hP : P y = 0 ∧ 2 * P y ≠ 0), False
rwa₁ : ∀ (hP : Eq.{r + 1} (α := R) 0 0 ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
rwa₂ : ∀ (hP : True ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
rwa₃ : ∀ (hP : HMul.hMul (α := R) 2 0 ≠ 0), False
⊢ False
have rwa₄ : ∀ (hP : Ne.{r + 1} (α := R) 0 0), False
Tactic: rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : HPow.hPow (β := ℕ) (P y) 2 = 0 ∧ 2 * P y ≠ 0
rwa : ∀ (hP : P y = 0 ∧ 2 * P y ≠ 0), False
rwa₁ : ∀ (hP : Eq.{r + 1} (α := R) 0 0 ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
rwa₂ : ∀ (hP : True ∧ HMul.hMul (α := R) 2 0 ≠ 0), False
rwa₃ : ∀ (hP : HMul.hMul (α := R) 2 0 ≠ 0), False
rwa₄ : ∀ (hP : Ne.{r + 1} (α := R) 0 0), False
⊢ False
have rwa₅ : ∀ (hP : False), False
Tactic: rwa [pow_eq_zero_iff two_ne_zero, hP.left, eq_self, true_and, mul_zero, ne_self_iff_false] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P y ≠ 0
have hPx : P x ≠ 0
Tactic: have hPx : P x ≠ 0 := X_ne_zero_of_Z_eq_zero hP hPz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False
have hP₁ : 0 = HPow.hPow (β := ℕ) (P x) 3 ∧ (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ HMul.hMul (α := R) 2 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
Tactic: rw [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPy, zero_pow two_ne_zero] at hP
Cleared hypotheses: hP, hPz, hPx, hPy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 hPx : IsUnit (P x)
Tactic: have hPx : IsUnit <| P x := isUnit_X_of_Z_eq_zero hP hPz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
⊢ P ≈ Q
have hPy : IsUnit (P y)
Tactic: have hPy : IsUnit <| P y := isUnit_Y_of_Z_eq_zero hP hPz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
⊢ P ≈ Q
have hQx : IsUnit (Q x)
Tactic: have hQx : IsUnit <| Q x := isUnit_X_of_Z_eq_zero hQ hQz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
⊢ P ≈ Q
have hQy : IsUnit (Q y)
Tactic: have hQy : IsUnit <| Q y := isUnit_Y_of_Z_eq_zero hQ hQz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
⊢ P ≈ Q
have hP₁ : HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
  (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
Tactic: simp only [nonsingular_of_Z_eq_zero, equation_of_Z_eq_zero, hPz, hQz] at hP hQ
Cleared hypotheses: hP, hQ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP₁ :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
⊢ P ≈ Q
have hQ₁ : HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
  (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
Tactic: simp only [nonsingular_of_Z_eq_zero, equation_of_Z_eq_zero, hPz, hQz] at hP hQ
Cleared hypotheses: hP, hQ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ P ≈ Q
have h : (fun (m : Fˣ) ↦ m • Q) (hPy.unit / hPx.unit * (hQx.unit / hQy.unit)) = P
Tactic: use (hPy.unit / hPx.unit) * (hQx.unit / hQy.unit)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ (fun (m : Fˣ) ↦ m • Q) (hPy.unit / hPx.unit * (hQx.unit / hQy.unit)) = P
have h : ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x,
    HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 *
        (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y,
    0] =
  P
Tactic: simp only [Units.smul_def, smul_fin3, Units.val_mul, Units.val_div_eq_div_val, IsUnit.unit_spec,
    mul_pow, div_pow, hQz, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
| P
have rw : ![P x, P y, 0]
Tactic: rw [← fin3_def P, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 *
          (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
        Q x,
      HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 *
          (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
        Q y,
      0] =
    P
have h : ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x,
    HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 *
        (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
      Q y,
    0] =
  ![P x, P y, 0]
Tactic: conv_rhs => rw [← fin3_def P, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 *
          (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
        Q x,
      HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 *
          (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
        Q y,
      0] =
    ![P x, P y, 0]
have h : HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
    Q x =
  P x
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
⊢ ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 *
          (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
        Q x,
      HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 *
          (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
        Q y,
      0] =
    ![P x, P y, 0]
have h₁ : HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3 * (HPow.hPow (β := ℕ) (Q x) 3 / HPow.hPow (β := ℕ) (Q y) 3) *
    Q y =
  P y
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
have h : HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
    Q x =
  P x
Tactic: rw [hP.left, pow_succ, (hPx.pow 2).mul_div_cancel_left, hQ.left, pow_succ _ 2,
      (hQx.pow 2).div_mul_cancel_left, hQx.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
⊢ HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
have h₁ : HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 *
      (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
    Q x =
  P x
Tactic: rw [hP.left, pow_succ, (hPx.pow 2).mul_div_cancel_left, hQ.left, pow_succ _ 2,
      (hQx.pow 2).div_mul_cancel_left, hQx.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₁ :
  HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 *
        (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
⊢ HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
have h₂ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) * Q x = P x
Tactic: rw [hP.left, pow_succ, (hPx.pow 2).mul_div_cancel_left, hQ.left, pow_succ _ 2,
      (hQx.pow 2).div_mul_cancel_left, hQx.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₁ :
  HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 *
        (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₂ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) * Q x = P x
⊢ HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
have h₃ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q x) 3) * Q x = P x
Tactic: rw [hP.left, pow_succ, (hPx.pow 2).mul_div_cancel_left, hQ.left, pow_succ _ 2,
      (hQx.pow 2).div_mul_cancel_left, hQx.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₁ :
  HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 *
        (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₂ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) * Q x = P x
h₃ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q x) 3) * Q x = P x
⊢ HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
have h₄ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / (HPow.hPow (β := ℕ) (Q x) 2 * Q x)) * Q x = P x
Tactic: rw [hP.left, pow_succ, (hPx.pow 2).mul_div_cancel_left, hQ.left, pow_succ _ 2,
      (hQx.pow 2).div_mul_cancel_left, hQx.inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP :
  HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (P x) 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ :
  HPow.hPow (β := ℕ) (Q y) 2 = HPow.hPow (β := ℕ) (Q x) 3 ∧
    (3 * HPow.hPow (β := ℕ) (Q x) 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
h :
  HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₁ :
  HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 *
        (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
h₂ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) * Q x = P x
h₃ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q x) 3) * Q x = P x
h₄ : P x * (HPow.hPow (β := ℕ) (Q x) 2 / (HPow.hPow (β := ℕ) (Q x) 2 * Q x)) * Q x = P x
⊢ HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * (HPow.hPow (β := ℕ) (Q x) 2 / HPow.hPow (β := ℕ) (Q y) 2) *
      Q x =
    P x
have h₅ : P x * (Q x)⁻¹ * Q x = P x
Tactic: rw [hP.left, pow_succ, (hPx.pow 2).mul_div_cancel_left, hQ.left, pow_succ _ 2,
      (hQx.pow 2).div_mul_cancel_left, hQx.inv_mul_cancel_right]