awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hP : W'.Equation P
⊢ W'.addY P (W'.neg P) = -HPow.hPow (β := ℕ) (W'.dblZ P) 3
have rw : -![HPow.hPow (β := ℕ) (W'.dblZ P) 2, HPow.hPow (β := ℕ) (W'.dblZ P) 3, 0] y = -HPow.hPow (β := ℕ) (W'.dblZ P) 3
Tactic: rw [addY, addX_neg hP, negAddY_neg hP, addZ_neg, negY_of_Z_eq_zero rfl]
-- 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
hP : W'.Equation P
⊢ W'.addXYZ P (W'.neg P) = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![1, 1, 0]
have rw : ![HPow.hPow (β := ℕ) (W'.dblZ P) 2, -HPow.hPow (β := ℕ) (W'.dblZ P) 3, 0] =
  ![HPow.hPow (β := ℕ) (-W'.dblZ P) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-W'.dblZ P) 3 * ![1, 1, 0] y,
    -W'.dblZ P * ![1, 1, 0] z]
Tactic: rw [addXYZ, addX_neg hP, addY_neg hP, addZ_neg, smul_fin3]
-- 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
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![1, 1, 0]⟧
have rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![1, 1, 0]⟧
Tactic: rw [negMap_eq, neg_of_Z_eq_zero hP hPz,
    smul_eq _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg]
-- 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
rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![1, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![1, 1, 0]⟧
have rw₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]⟧ ⟦![1, 1, 0]⟧
Tactic: rw [negMap_eq, neg_of_Z_eq_zero hP hPz,
    smul_eq _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg]
-- 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
rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![1, 1, 0]⟧
rw₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]⟧ ⟦![1, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![1, 1, 0]⟧
have rw₂ : Eq.{u + 1} (α := PointClass F) ⟦![1, 1, 0]⟧ ⟦![1, 1, 0]⟧
Tactic: rw [negMap_eq, neg_of_Z_eq_zero hP hPz,
    smul_eq _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg]
-- 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
hPz : P z ≠ 0
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧)
    ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
have rw : Eq (α := PointClass F) ⟦W.neg P⟧
  ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
      W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
Tactic: rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]
-- 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
hPz : P z ≠ 0
rw :
  Eq (α := PointClass F) ⟦W.neg P⟧
    ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧)
    ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
have rw₁ : Eq (α := PointClass F)
  ⟦P z •
      ![P x / HPow.hPow (β := ℕ) (P z) 2,
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
  ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
      W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
Tactic: rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]
-- 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
hPz : P z ≠ 0
rw :
  Eq (α := PointClass F) ⟦W.neg P⟧
    ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
rw₁ :
  Eq (α := PointClass F)
    ⟦P z •
        ![P x / HPow.hPow (β := ℕ) (P z) 2,
          W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
    ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧)
    ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
have rw₂ : Eq (α := PointClass F)
  ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
      W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
  ⟦![P x / HPow.hPow (β := ℕ) (P z) 2,
      W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]⟧
Tactic: rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : PointClass F
hP : W.NonsingularLift P
⊢ W.NonsingularLift (W.negMap P)
have mk : ∀ (a : Fin 3 → F)
  (hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)),
  W.NonsingularLift (W.negMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a))
Tactic: rcases P with ⟨_⟩
Cleared hypotheses: hP
-- 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
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) = HPow.hPow (β := ℕ) u 4 • W'.add P Q
have rw : W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.add P Q
Tactic: rw [add_of_equiv <| (smul_equiv_smul P Q hu hv).mpr h, dblXYZ_smul, add_of_equiv h]
-- 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
u v : R
hu : IsUnit u
hv : IsUnit v
rw : W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.add P Q
⊢ W'.add (u • P) (v • Q) = HPow.hPow (β := ℕ) u 4 • W'.add P Q
have rw₁ : HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P = HPow.hPow (β := ℕ) u 4 • W'.add P Q
Tactic: rw [add_of_equiv <| (smul_equiv_smul P Q hu hv).mpr h, dblXYZ_smul, add_of_equiv h]
-- 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
u v : R
hu : IsUnit u
hv : IsUnit v
rw : W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.add P Q
rw₁ : HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P = HPow.hPow (β := ℕ) u 4 • W'.add P Q
⊢ W'.add (u • P) (v • Q) = HPow.hPow (β := ℕ) u 4 • W'.add P Q
have rw₂ : HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
Tactic: rw [add_of_equiv <| (smul_equiv_smul P Q hu hv).mpr h, dblXYZ_smul, add_of_equiv h]
-- 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
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
have rw : W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
Tactic: rw [add_of_not_equiv <| h.comp (smul_equiv_smul P Q hu hv).mp, addXYZ_smul, add_of_not_equiv h]
-- 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
u v : R
hu : IsUnit u
hv : IsUnit v
rw : W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
⊢ W'.add (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
have rw₁ : HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
Tactic: rw [add_of_not_equiv <| h.comp (smul_equiv_smul P Q hu hv).mp, addXYZ_smul, add_of_not_equiv h]
-- 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
u v : R
hu : IsUnit u
hv : IsUnit v
rw : W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
rw₁ : HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
⊢ W'.add (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
have rw₂ : HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
Tactic: rw [add_of_not_equiv <| h.comp (smul_equiv_smul P Q hu hv).mp, addXYZ_smul, add_of_not_equiv h]
-- 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
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q
have pos : ∀ (h : P ≈ Q), W'.add (u • P) (v • Q) ≈ W'.add P Q
Tactic: by_cases h : P ≈ Q
-- 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
u v : R
hu : IsUnit u
hv : IsUnit v
pos : ∀ (h : P ≈ Q), W'.add (u • P) (v • Q) ≈ W'.add P Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q
have neg : ∀ (h : ¬P ≈ Q), W'.add (u • P) (v • Q) ≈ W'.add P Q
Tactic: by_cases h : P ≈ Q
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P P' Q Q' : Fin 3 → R
hP : P ≈ P'
hQ : Q ≈ Q'
⊢ W'.add P Q ≈ W'.add P' Q'
have rcases : ∀ (u v : Rˣ), W'.add ((fun (m : Rˣ) ↦ m • P') u) ((fun (m : Rˣ) ↦ m • Q') v) ≈ W'.add P' Q'
Tactic: rcases hP, hQ with ⟨⟨u, rfl⟩, ⟨v, rfl⟩⟩
Cleared hypotheses: P, Q, hP, hQ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]
have rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]
Tactic: rw [add_of_equiv <| equiv_of_Z_eq_zero hP hQ hPz hQz, dblXYZ_of_Z_eq_zero hP.left hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
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
rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]
have rw₁ : HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0] =
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]
Tactic: rw [add_of_equiv <| equiv_of_Z_eq_zero hP hQ hPz hQz, dblXYZ_of_Z_eq_zero hP.left hPz]
-- 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
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
⊢ W'.add P Q = (P x * Q z) • Q
have rw : W'.addXYZ P Q = (P x * Q z) • Q
Tactic: rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]
-- 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
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
rw : W'.addXYZ P Q = (P x * Q z) • Q
⊢ W'.add P Q = (P x * Q z) • Q
have rw₁ : (P x * Q z) • Q = (P x * Q z) • Q
Tactic: rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]
-- 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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
⊢ W'.add P Q = -(Q x * P z) • P
have rw : W'.addXYZ P Q = -(Q x * P z) • P
Tactic: rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_right hPz hQz, addXYZ_of_Z_eq_zero_right hQ hQz]
-- 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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
rw : W'.addXYZ P Q = -(Q x * P z) • P
⊢ W'.add P Q = -(Q x * P z) • P
have rw₁ : -(Q x * P z) • P = -(Q x * P z) • P
Tactic: rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_right hPz hQz, addXYZ_of_Z_eq_zero_right hQ hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0]
have rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0]
Tactic: rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hQz hx hy hy']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0]
have rw₁ : HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0] =
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0]
Tactic: rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hQz hx hy hy']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
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 ≠ Q y * HPow.hPow (β := ℕ) (P z) 3
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]
have rw : W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]
Tactic: rw [add_of_not_equiv <| not_equiv_of_Y_ne hy, addXYZ_of_X_eq hP hQ hPz hQz hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
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 ≠ Q y * HPow.hPow (β := ℕ) (P z) 3
rw : W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]
have rw₁ : HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0] =
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]
Tactic: rw [add_of_not_equiv <| not_equiv_of_Y_ne hy, addXYZ_of_X_eq hP hQ hPz hQz hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
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.add P Q =
    W.dblZ P •
      ![W.toAffine.addX (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.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / 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)),
        1]
have rw : W.dblXYZ P =
  W.dblZ P •
    ![W.toAffine.addX (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.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / 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)),
      1]
Tactic: rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx <| Y_eq_of_Y_ne' hP hQ hx hy,
    dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
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
rw :
  W.dblXYZ P =
    W.dblZ P •
      ![W.toAffine.addX (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.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / 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)),
        1]
⊢ W.add P Q =
    W.dblZ P •
      ![W.toAffine.addX (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.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / 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)),
        1]
have rw₁ : W.dblZ P •
    ![W.toAffine.addX (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.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / 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)),
      1] =
  W.dblZ P •
    ![W.toAffine.addX (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.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / 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)),
      1]
Tactic: rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx <| Y_eq_of_Y_ne' hP hQ hx hy,
    dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 ≠ Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ W.add P Q =
    addZ P Q •
      ![W.toAffine.addX (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.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / 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)),
        1]
have rw : W.addXYZ P Q =
  addZ P Q •
    ![W.toAffine.addX (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.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / 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)),
      1]
Tactic: rw [add_of_not_equiv <| not_equiv_of_X_ne hx, addXYZ_of_Z_ne_zero hP hQ hPz hQz hx]