awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
erw :
  ![W'.addX P (W'.neg P), W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₁ :
  ![0, W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₂ :
  ![0, -W'.dblZ P, W'.addZ P (W'.neg P)] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
⊢ W'.addXYZ P (W'.neg P) = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
have erw₃ : ![0, -W'.dblZ P, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
Tactic: erw [addXYZ, addX_neg, addY_neg hP, addZ_neg, smul_fin3, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
erw :
  ![W'.addX P (W'.neg P), W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₁ :
  ![0, W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₂ :
  ![0, -W'.dblZ P, W'.addZ P (W'.neg P)] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₃ : ![0, -W'.dblZ P, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
⊢ W'.addXYZ P (W'.neg P) = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
have erw₄ : ![0, -W'.dblZ P, 0] = ![-W'.dblZ P * ![0, 1, 0] x, -W'.dblZ P * ![0, 1, 0] y, -W'.dblZ P * ![0, 1, 0] z]
Tactic: erw [addXYZ, addX_neg, addY_neg hP, addZ_neg, smul_fin3, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
erw :
  ![W'.addX P (W'.neg P), W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₁ :
  ![0, W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₂ :
  ![0, -W'.dblZ P, W'.addZ P (W'.neg P)] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₃ : ![0, -W'.dblZ P, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₄ : ![0, -W'.dblZ P, 0] = ![-W'.dblZ P * ![0, 1, 0] x, -W'.dblZ P * ![0, 1, 0] y, -W'.dblZ P * ![0, 1, 0] z]
⊢ W'.addXYZ P (W'.neg P) = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
have erw₅ : ![0, -W'.dblZ P, 0] = ![0, -W'.dblZ P * ![0, 1, 0] y, 0]
Tactic: erw [addXYZ, addX_neg, addY_neg hP, addZ_neg, smul_fin3, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
erw :
  ![W'.addX P (W'.neg P), W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₁ :
  ![0, W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₂ :
  ![0, -W'.dblZ P, W'.addZ P (W'.neg P)] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₃ : ![0, -W'.dblZ P, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₄ : ![0, -W'.dblZ P, 0] = ![-W'.dblZ P * ![0, 1, 0] x, -W'.dblZ P * ![0, 1, 0] y, -W'.dblZ P * ![0, 1, 0] z]
erw₅ : ![0, -W'.dblZ P, 0] = ![0, -W'.dblZ P * ![0, 1, 0] y, 0]
⊢ W'.addXYZ P (W'.neg P) = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
have erw₆ : ![0, -W'.dblZ P, 0] = ![0, -W'.dblZ P, 0]
Tactic: erw [addXYZ, addX_neg, addY_neg hP, addZ_neg, smul_fin3, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![0, 1, 0]⟧
have rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![0, 1, 0]⟧
Tactic: rw [negMap_eq, neg_of_Z_eq_zero hP.left hPz, smul_eq _ (isUnit_Y_of_Z_eq_zero hP hPz).neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![0, 1, 0]⟧
have rw₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-P y) ![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
Tactic: rw [negMap_eq, neg_of_Z_eq_zero hP.left hPz, smul_eq _ (isUnit_Y_of_Z_eq_zero hP hPz).neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![0, 1, 0]⟧
rw₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-P y) ![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![0, 1, 0]⟧
have rw₂ : Eq.{u + 1} (α := PointClass F) ⟦![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
Tactic: rw [negMap_eq, neg_of_Z_eq_zero hP.left hPz, smul_eq _ (isUnit_Y_of_Z_eq_zero hP hPz).neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
have rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
Tactic: rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
have rw₁ : Eq (α := PointClass F) ⟦P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
  ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
Tactic: rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
rw₁ :
  Eq (α := PointClass F) ⟦P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
    ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
have rw₂ : Eq (α := PointClass F) ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
  ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
Tactic: rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 y) 4) ![0, 1, 0]
have rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 y) 4) ![0, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
have rw₁ : HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0] =
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
⊢ W'.add P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
have rw : W'.addXYZ P Q = (HPow.hPow (β := ℕ) (P y) 2 * 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
rw : W'.addXYZ P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
⊢ W'.add P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
have rw₁ : (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q = (HPow.hPow (β := ℕ) (P y) 2 * 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
⊢ W'.add P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
have rw : W'.addXYZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
rw : W'.addXYZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
⊢ W'.add P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
have rw₁ : -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P = -(HPow.hPow (β := ℕ) (Q y) 2 * 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
have rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
Tactic: rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hP hPz hQz hx hy hy']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
have rw₁ : HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0] =
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
Tactic: rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hP hPz hQz hx hy hy']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
have rw : W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
rw : W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
have rw₁ : HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0] =
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.add P Q =
    W.dblZ P •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]
have rw : W.dblXYZ P =
  W.dblZ P •
    ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      1]
Tactic: rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx <| Y_eq_of_Y_ne' hP hQ hPz hQz hx hy,
    dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
rw :
  W.dblXYZ P =
    W.dblZ P •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]
⊢ W.add P Q =
    W.dblZ P •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]
have rw₁ : W.dblZ P •
    ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      1] =
  W.dblZ P •
    ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      1]
Tactic: rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx <| Y_eq_of_Y_ne' hP hQ hPz hQz hx hy,
    dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z ≠ Q x * P z
⊢ W.add P Q =
    W.addZ P Q •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]
have rw : W.addXYZ P Q =
  W.addZ P Q •
    ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      1]
Tactic: rw [add_of_not_equiv <| not_equiv_of_X_ne hx, addXYZ_of_Z_ne_zero hP hQ hPz hQz hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z ≠ Q x * P z
rw :
  W.addXYZ P Q =
    W.addZ P Q •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]
⊢ W.add P Q =
    W.addZ P Q •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]
have rw₁ : W.addZ P Q •
    ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      1] =
  W.addZ P Q •
    ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      1]
Tactic: rw [add_of_not_equiv <| not_equiv_of_X_ne hx, addXYZ_of_Z_ne_zero hP hQ hPz hQz hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x / P z = Q x / Q z ∧ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z))
have rwa : ¬(P x * Q z = Q x * P z ∧ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z))
Tactic: rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ W.Nonsingular (W.add P Q)
have pos : ∀ (hPz : P z = 0), W.Nonsingular (W.add P Q)
Tactic: by_cases hPz : P z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
pos : ∀ (hPz : P z = 0), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)
have neg : ∀ (hPz : ¬P z = 0), W.Nonsingular (W.add P Q)
Tactic: by_cases hPz : P z = 0