awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addX P Q)
rw₁ :
  (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((W'⁄A).map (↑f : A →+* B)).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
⊢ (W'⁄B).addX ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).addX P Q)
have rw₂ : (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← map_addX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).negAddY ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).negAddY P Q)
have rw : (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negAddY P Q)
Tactic: rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negAddY P Q)
⊢ (W'⁄B).negAddY ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).negAddY P Q)
have rw₁ : (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  ((W'⁄A).map (↑f : A →+* B)).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negAddY P Q)
rw₁ :
  (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((W'⁄A).map (↑f : A →+* B)).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
⊢ (W'⁄B).negAddY ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).negAddY P Q)
have rw₂ : (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).addY ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).addY P Q)
have rw : (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addY P Q)
Tactic: rw [← RingHom.coe_coe, ← map_addY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addY P Q)
⊢ (W'⁄B).addY ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).addY P Q)
have rw₁ : (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  ((W'⁄A).map (↑f : A →+* B)).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← map_addY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addY P Q)
rw₁ :
  (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((W'⁄A).map (↑f : A →+* B)).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
⊢ (W'⁄B).addY ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).addY P Q)
have rw₂ : (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← map_addY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).addXYZ ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (⇑f : (a : A) → B) ∘ (W'⁄A).addXYZ P Q
have rw : (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).addXYZ P Q
Tactic: rw [← RingHom.coe_coe, ← map_addXYZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).addXYZ P Q
⊢ (W'⁄B).addXYZ ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (⇑f : (a : A) → B) ∘ (W'⁄A).addXYZ P Q
have rw₁ : (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  ((W'⁄A).map (↑f : A →+* B)).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← map_addXYZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Jacobian R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).addXYZ P Q
rw₁ :
  (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((W'⁄A).map (↑f : A →+* B)).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
⊢ (W'⁄B).addXYZ ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (⇑f : (a : A) → B) ∘ (W'⁄A).addXYZ P Q
have rw₂ : (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
  (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← map_addXYZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.neg (u • P) = u • W'.neg P
have rw : ![(u • P) x, HPow.hPow (β := ℕ) u 3 * W'.negY P, (u • P) z] = u • W'.neg P
Tactic: rw [neg, negY_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.neg P ≈ W'.neg Q
have rcases : ∀ (u : Rˣ), W'.neg ((fun (m : Rˣ) ↦ m • Q) u) ≈ W'.neg Q
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.neg P = ![P x, -P y, 0]
have rw : ![P x, W'.negY P, P z] = ![P x, -P y, 0]
Tactic: rw [neg, negY_of_Z_eq_zero hPz, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : ![P x, W'.negY P, P z] = ![P x, -P y, 0]
⊢ W'.neg P = ![P x, -P y, 0]
have rw₁ : ![P x, -P y, P z] = ![P x, -P y, 0]
Tactic: rw [neg, negY_of_Z_eq_zero hPz, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : ![P x, W'.negY P, P z] = ![P x, -P y, 0]
rw₁ : ![P x, -P y, P z] = ![P x, -P y, 0]
⊢ W'.neg P = ![P x, -P y, 0]
have rw₂ : ![P x, -P y, 0] = ![P x, -P y, 0]
Tactic: rw [neg, negY_of_Z_eq_zero hPz, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
Tactic: have hX {n : ℕ} : IsUnit <| P x ^ n := (isUnit_X_of_Z_eq_zero hP hPz).pow n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₁ : ![P x, -P y, 0] =
  ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
    -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₂ : ![P x, -P y, 0] =
  ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
    -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₃ : ![P x, -P y, 0] =
  ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
    HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₄ : ![P x, -P y, 0] =
  ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
    HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₅ : ![P x, -P y, 0] =
  ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
    HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₆ : ![P x, -P y, 0] = ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₆ :
  ![P x, -P y, 0] =
    ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₇ : ![P x, -P y, 0] = ![P x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₆ :
  ![P x, -P y, 0] =
    ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₇ : ![P x, -P y, 0] = ![P x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₈ : ![P x, -P y, 0] = ![P x, -HPow.hPow (β := ℕ) (P y / P x) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]