awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ W.Nonsingular (W.add P Q)
have pos : ∀ (hQz : Q z = 0), W.Nonsingular (W.add P Q)
Tactic: by_cases hQz : Q 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
hPz : P z = 0
pos : ∀ (hQz : Q z = 0), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)
have neg : ∀ (hQz : ¬Q z = 0), W.Nonsingular (W.add P Q)
Tactic: by_cases hQz : Q 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
hPz : ¬P z = 0
⊢ W.Nonsingular (W.add P Q)
have pos : ∀ (hQz : Q z = 0), W.Nonsingular (W.add P Q)
Tactic: by_cases hQz : Q 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
hPz : ¬P z = 0
pos : ∀ (hQz : Q z = 0), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)
have neg : ∀ (hQz : ¬Q z = 0), W.Nonsingular (W.add P Q)
Tactic: by_cases hQz : Q 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
hPz : ¬P z = 0
hQz : ¬Q z = 0
⊢ W.Nonsingular (W.add P Q)
have pos : ∀ (hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z), W.Nonsingular (W.add P Q)
Tactic: by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
-- 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
pos : ∀ (hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)
have neg : ∀ (hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)), W.Nonsingular (W.add P Q)
Tactic: by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
-- 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
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
⊢ W.Nonsingular (W.add P Q)
have pos : ∀ (hy : P y * Q z = Q y * P z), W.Nonsingular (W.add P Q)
Tactic: by_cases hy : P y * Q z = Q y * P z
-- 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
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
pos : ∀ (hy : P y * Q z = Q y * P z), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)
have neg : ∀ (hy : ¬P y * Q z = Q y * P z), W.Nonsingular (W.add P Q)
Tactic: by_cases hy : P y * Q z = Q y * P z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (hypothesis)
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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ W.Nonsingular (W.add P Q)
have this : W.Nonsingular
  ![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: have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
-- 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
this :
  W.Nonsingular
    ![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.Nonsingular (W.add P Q)
have pos : ∀ (hx : P x * Q z = Q x * P z), W.Nonsingular (W.add P Q)
Tactic: by_cases hx : P x * Q z = Q x * P z
-- 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
this :
  W.Nonsingular
    ![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]
pos : ∀ (hx : P x * Q z = Q x * P z), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)
have neg : ∀ (hx : ¬P x * Q z = Q x * P z), W.Nonsingular (W.add P Q)
Tactic: by_cases hx : P x * Q z = Q x * P z
-- 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ W.Nonsingular (W.add P Q)
have neg : ∀
  (this :
    W.Nonsingular
      ![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.Nonsingular (W.add P Q)
Tactic: classical
        have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
        by_cases hx : P x * Q z = Q x * P z
        · simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hQz hx <|
              not_and.mp hxy hx]
        · simpa only [add_of_X_ne hP.left hQ.left hPz hQz hx,
            nonsingular_smul _ <| isUnit_addZ_of_X_ne hP.left hQ.left 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.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)
neg neg₁ neg₂ :
  ∀
    (this :
      W.Nonsingular
        ![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.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)
have pos : ∀
  (this :
    W.Nonsingular
      ![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])
  (hx : P x * Q z = Q x * P z), W.Nonsingular (W.add P Q)
Tactic: classical
        have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
        by_cases hx : P x * Q z = Q x * P z
        · simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hQz hx <|
              not_and.mp hxy hx]
        · simpa only [add_of_X_ne hP.left hQ.left hPz hQz hx,
            nonsingular_smul _ <| isUnit_addZ_of_X_ne hP.left hQ.left 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.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)
neg neg₁ neg₂ :
  ∀
    (this :
      W.Nonsingular
        ![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.Nonsingular (W.add P Q)
pos :
  ∀
    (this :
      W.Nonsingular
        ![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])
    (hx : P x * Q z = Q x * P z), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)
have neg₃ : ∀
  (this :
    W.Nonsingular
      ![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])
  (hx : ¬P x * Q z = Q x * P z), W.Nonsingular (W.add P Q)
Tactic: classical
        have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
        by_cases hx : P x * Q z = Q x * P z
        · simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hQz hx <|
              not_and.mp hxy hx]
        · simpa only [add_of_X_ne hP.left hQ.left hPz hQz hx,
            nonsingular_smul _ <| isUnit_addZ_of_X_ne hP.left hQ.left hx]
-- 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
Q : PointClass F
hP : W.Nonsingular P
hQ : W.NonsingularLift Q
hPz : P z = 0
⊢ W.addMap ⟦P⟧ Q = Q
have revert : ∀ (hQ : W.NonsingularLift Q), W.addMap ⟦P⟧ Q = Q
Tactic: revert hQ
Cleared hypotheses: hQ
-- 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
Q : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
⊢ ∀ (hQ : W.NonsingularLift Q), W.addMap ⟦P⟧ Q = Q
have refine : ∀ (Q : Fin 3 → F) (hQ : W.NonsingularLift ⟦Q⟧), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
Tactic: refine Q.inductionOn (motive := fun Q => _ → W.addMap _ Q = Q) fun Q hQ => ?_
-- 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
Q_1 : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
have pos : ∀ (hQz : Q z = 0), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
Tactic: by_cases hQz : Q 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
Q_1 : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
pos : ∀ (hQz : Q z = 0), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
have neg : ∀ (hQz : ¬Q z = 0), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
Tactic: by_cases hQz : Q 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
Q_1 : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : Q z = 0
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
have pos : (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![0, 1, 0] Q
Tactic: rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, Quotient.eq]
-- 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
Q_1 : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : ¬Q z = 0
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
have neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦Q⟧
Tactic: rw [addMap_eq, add_of_Z_eq_zero_left hP.left hPz hQz,
      smul_eq _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]
-- 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
Q_1 : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : ¬Q z = 0
neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦Q⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
have neg₁ : Eq (α := PointClass F) ⟦(HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q⟧ ⟦Q⟧
Tactic: rw [addMap_eq, add_of_Z_eq_zero_left hP.left hPz hQz,
      smul_eq _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]
-- 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
Q_1 : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : ¬Q z = 0
neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦Q⟧
neg₁ : Eq (α := PointClass F) ⟦(HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q⟧ ⟦Q⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
have neg₂ : Eq (α := PointClass F) ⟦Q⟧ ⟦Q⟧
Tactic: rw [addMap_eq, add_of_Z_eq_zero_left hP.left hPz hQz,
      smul_eq _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : PointClass F
Q : Fin 3 → F
hP : W.NonsingularLift P
hQ : W.Nonsingular Q
hQz : Q z = 0
⊢ W.addMap P ⟦Q⟧ = P
have revert : ∀ (hP : W.NonsingularLift P), W.addMap P ⟦Q⟧ = P
Tactic: revert hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
⊢ ∀ (hP : W.NonsingularLift P), W.addMap P ⟦Q⟧ = P
have refine : ∀ (P : Fin 3 → F) (hP : W.NonsingularLift ⟦P⟧), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
Tactic: refine P.inductionOn (motive := fun P => _ → W.addMap P _ = P) fun P hP => ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
have pos : ∀ (hPz : P z = 0), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦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_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
pos : ∀ (hPz : P z = 0), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
have neg : ∀ (hPz : ¬P z = 0), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦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_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
have pos : (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![0, 1, 0] P
Tactic: rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, Quotient.eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
have neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦P⟧
Tactic: rw [addMap_eq, add_of_Z_eq_zero_right hQ.left hPz hQz,
      smul_eq _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦P⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
have neg₁ : Eq (α := PointClass F) ⟦-(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P⟧ ⟦P⟧
Tactic: rw [addMap_eq, add_of_Z_eq_zero_right hQ.left hPz hQz,
      smul_eq _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦P⟧
neg₁ : Eq (α := PointClass F) ⟦-(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P⟧ ⟦P⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
have neg₂ : Eq (α := PointClass F) ⟦P⟧ ⟦P⟧
Tactic: rw [addMap_eq, add_of_Z_eq_zero_right hQ.left hPz hQz,
      smul_eq _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]
-- 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.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
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
have pos : ∀ (hy : P y * Q z = Q y * P z), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
Tactic: by_cases hy : P y * Q z = Q y * P z
-- 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.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
pos : ∀ (hy : P y * Q z = Q y * P z), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
have neg : ∀ (hy : ¬P y * Q z = Q y * P z), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
Tactic: by_cases hy : P y * Q z = Q y * P z
-- 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.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
hy : P y * Q z = Q y * P z
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
have pos : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦![0, 1, 0]⟧
Tactic: rw [addMap_eq, add_of_Y_eq hP.left hPz hQz hx hy hy',
      smul_eq _ <| isUnit_dblU_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.Nonsingular 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
hy : P y * Q z = Q y * P z
pos : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
have pos₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
Tactic: rw [addMap_eq, add_of_Y_eq hP.left hPz hQz hx hy hy',
      smul_eq _ <| isUnit_dblU_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.Nonsingular 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
hy : P y * Q z = Q y * P z
pos : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦![0, 1, 0]⟧
pos₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
have pos₂ : Eq.{u + 1} (α := PointClass F) ⟦![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
Tactic: rw [addMap_eq, add_of_Y_eq hP.left hPz hQz hx hy hy',
      smul_eq _ <| isUnit_dblU_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.Nonsingular 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
hy : ¬P y * Q z = Q y * P z
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
have neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦![0, 1, 0]⟧
Tactic: rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy,
      smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz 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.Nonsingular 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
hy : ¬P y * Q z = Q y * P z
neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
have neg₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
Tactic: rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy,
      smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz 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.Nonsingular 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
hy : ¬P y * Q z = Q y * P z
neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦![0, 1, 0]⟧
neg₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![0, 1, 0]⟧
have neg₂ : Eq.{u + 1} (α := PointClass F) ⟦![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
Tactic: rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy,
      smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ Eq (α := PointClass F) (W.addMap ⟦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 pos : ∀ (hx : P x * Q z = Q x * P z),
  Eq (α := PointClass F) (W.addMap ⟦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: by_cases hx : P x * Q z = Q x * P z