awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.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' : Projective 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.Projective.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' : Projective 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.Projective.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' : Projective 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.Projective.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' : Projective 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.Projective.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' : Projective 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.Projective.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' : Projective 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.Projective.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' : Projective 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.Projective.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' : Projective 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.Projective.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' : Projective 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.Projective.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' : Projective 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.Projective.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.neg P = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
have erw : ![P x, W.negY P, P z] = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
Tactic: erw [neg, smul_fin3, mul_div_cancel₀ _ hPz, ← negY_of_Z_ne_zero hPz, mul_div_cancel₀ _ hPz,
    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
hPz : P z ≠ 0
erw : ![P x, W.negY P, P z] = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
⊢ W.neg P = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
have erw₁ : ![P x, W.negY P, P z] =
  ![P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] x,
    P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
    P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
Tactic: erw [neg, smul_fin3, mul_div_cancel₀ _ hPz, ← negY_of_Z_ne_zero hPz, mul_div_cancel₀ _ hPz,
    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
hPz : P z ≠ 0
erw : ![P x, W.negY P, P z] = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
erw₁ :
  ![P x, W.negY P, P z] =
    ![P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] x,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
⊢ W.neg P = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
have erw₂ : ![P x, W.negY P, P z] =
  ![P x, P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
    P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
Tactic: erw [neg, smul_fin3, mul_div_cancel₀ _ hPz, ← negY_of_Z_ne_zero hPz, mul_div_cancel₀ _ hPz,
    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
hPz : P z ≠ 0
erw : ![P x, W.negY P, P z] = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
erw₁ :
  ![P x, W.negY P, P z] =
    ![P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] x,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
erw₂ :
  ![P x, W.negY P, P z] =
    ![P x, P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
⊢ W.neg P = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
have erw₃ : ![P x, W.negY P, P z] = ![P x, P z * ![P x / P z, W.negY P / P z, 1] y, P z * ![P x / P z, W.negY P / P z, 1] z]
Tactic: erw [neg, smul_fin3, mul_div_cancel₀ _ hPz, ← negY_of_Z_ne_zero hPz, mul_div_cancel₀ _ hPz,
    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
hPz : P z ≠ 0
erw : ![P x, W.negY P, P z] = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
erw₁ :
  ![P x, W.negY P, P z] =
    ![P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] x,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
erw₂ :
  ![P x, W.negY P, P z] =
    ![P x, P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
erw₃ : ![P x, W.negY P, P z] = ![P x, P z * ![P x / P z, W.negY P / P z, 1] y, P z * ![P x / P z, W.negY P / P z, 1] z]
⊢ W.neg P = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
have erw₄ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z * ![P x / P z, W.negY P / P z, 1] z]
Tactic: erw [neg, smul_fin3, mul_div_cancel₀ _ hPz, ← negY_of_Z_ne_zero hPz, mul_div_cancel₀ _ hPz,
    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
hPz : P z ≠ 0
erw : ![P x, W.negY P, P z] = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
erw₁ :
  ![P x, W.negY P, P z] =
    ![P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] x,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
erw₂ :
  ![P x, W.negY P, P z] =
    ![P x, P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
erw₃ : ![P x, W.negY P, P z] = ![P x, P z * ![P x / P z, W.negY P / P z, 1] y, P z * ![P x / P z, W.negY P / P z, 1] z]
erw₄ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z * ![P x / P z, W.negY P / P z, 1] z]
⊢ W.neg P = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
have erw₅ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z]
Tactic: erw [neg, smul_fin3, mul_div_cancel₀ _ hPz, ← negY_of_Z_ne_zero hPz, mul_div_cancel₀ _ hPz,
    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
⊢ W.Nonsingular (W.neg P)
have pos : ∀ (hPz : P z = 0), W.Nonsingular (W.neg P)
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 : Fin 3 → F
hP : W.Nonsingular P
pos : ∀ (hPz : P z = 0), W.Nonsingular (W.neg P)
⊢ W.Nonsingular (W.neg P)
have neg : ∀ (hPz : ¬P z = 0), W.Nonsingular (W.neg P)
Tactic: by_cases hPz : P z = 0
-- 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
⊢ W'.addZ P (W'.neg P) = 0
have rw : -3 * HPow.hPow (β := ℕ) (P x) 2 * P x * P z + 3 * P x * HPow.hPow (β := ℕ) (P x) 2 * P z +
                      HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                    HPow.hPow (β := ℕ) (-P y - W'.a₁ * P x - W'.a₃ * P z) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * HPow.hPow (β := ℕ) (P z) 2 -
              W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (P z) 2 -
        W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * HPow.hPow (β := ℕ) (P z) 2 * P z -
      W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 +
    W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
  0
Tactic: rw [addZ, neg_X, neg_Y, neg_Z, negY]
-- 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
⊢ W'.addX P (W'.neg P) = 0
have rw : -P x * HPow.hPow (β := ℕ) (-P y - W'.a₁ * P x - W'.a₃ * P z) 2 * P z + P x * HPow.hPow (β := ℕ) (P y) 2 * P z -
                              2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                            2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z -
                          W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                        W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 * P y * P z +
                      W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P x * P z -
                    W'.a₂ * P x * HPow.hPow (β := ℕ) (P x) 2 * P z -
                  W'.a₃ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₃ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * HPow.hPow (β := ℕ) (P z) 2 -
              2 * W'.a₃ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z * P z +
            2 * W'.a₃ * P x * P y * P z * P z +
          W'.a₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
        W'.a₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
      3 * W'.a₆ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 -
    3 * W'.a₆ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
  0
Tactic: rw [addX, neg_X, neg_Y, neg_Z, negY]
-- 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
⊢ W'.negAddY P (W'.neg P) + -3 * (P y - W'.negY P) * 0 -
      (W'.dblZ P +
        -3 * (P y - W'.negY P) *
          (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
    0
have a : -3 * HPow.hPow (β := ℕ) (P x) 2 * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) +
                                        3 * P x * HPow.hPow (β := ℕ) (P x) 2 * P y -
                                      HPow.hPow (β := ℕ) (P y) 2 * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                                    P y * HPow.hPow (β := ℕ) (-P y - W'.a₁ * P x - W'.a₃ * P z) 2 * P z +
                                  W'.a₁ * P x * HPow.hPow (β := ℕ) (-P y - W'.a₁ * P x - W'.a₃ * P z) 2 * P z -
                                W'.a₁ * P x * HPow.hPow (β := ℕ) (P y) 2 * P z -
                              W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                            W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P y * P z +
                          2 * W'.a₂ * P x * P x * P y * P z -
                        2 * W'.a₂ * P x * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z -
                      W'.a₃ * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                    W'.a₃ * HPow.hPow (β := ℕ) (-P y - W'.a₁ * P x - W'.a₃ * P z) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₄ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 -
                2 * W'.a₄ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z * P z +
              2 * W'.a₄ * P x * P y * P z * P z -
            W'.a₄ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * HPow.hPow (β := ℕ) (P z) 2 +
          3 * W'.a₆ * P y * P z * HPow.hPow (β := ℕ) (P z) 2 -
        3 * W'.a₆ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * HPow.hPow (β := ℕ) (P z) 2 * P z +
      -3 * (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * 0 -
    (P z * HPow.hPow (β := ℕ) (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) 3 +
      -3 * (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) *
        (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
  0
Tactic: rw [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]
-- 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
⊢ W'.negAddY P (W'.neg P) = W'.dblZ P
have a : W'.negAddY P (W'.neg P) + -3 * (P y - W'.negY P) * 0 -
    (W'.dblZ P +
      -3 * (P y - W'.negY P) *
        (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
  0
Tactic: linear_combination (norm := (rw [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
    -3 * (P y - W'.negY P) * (equation_iff _).mp hP
-- 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
⊢ W'.addXYZ P (W'.neg P) = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
have 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]
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]
⊢ 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'.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]
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]
⊢ 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, W'.addZ P (W'.neg P)] = 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]