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
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)
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]⟧
⊢ 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 neg : ∀ (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
-- 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)
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]⟧
have pos : Eq (α := PointClass F) ⟦W.add 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 [addMap_eq, add_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy hx,
      smul_eq _ <| isUnit_dblZ_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
hx : P x * Q z = Q x * P z
pos :
  Eq (α := PointClass F) ⟦W.add 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]⟧
⊢ 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₁ : Eq (α := PointClass F)
  ⟦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.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 [addMap_eq, add_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy hx,
      smul_eq _ <| isUnit_dblZ_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
hx : P x * Q z = Q x * P z
pos :
  Eq (α := PointClass F) ⟦W.add 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]⟧
pos₁ :
  Eq (α := PointClass F)
    ⟦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.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]⟧
⊢ 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₂ : Eq (α := PointClass F)
  ⟦![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.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 [addMap_eq, add_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy hx,
      smul_eq _ <| isUnit_dblZ_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
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]⟧
have neg : Eq (α := PointClass F) ⟦W.add 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 [addMap_eq, add_of_X_ne hP hQ hPz hQz hx, smul_eq _ <| isUnit_addZ_of_X_ne hP hQ 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
hx : ¬P x * Q z = Q x * P z
neg :
  Eq (α := PointClass F) ⟦W.add 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]⟧
⊢ 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 neg₁ : Eq (α := PointClass F)
  ⟦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.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 [addMap_eq, add_of_X_ne hP hQ hPz hQz hx, smul_eq _ <| isUnit_addZ_of_X_ne hP hQ 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
hx : ¬P x * Q z = Q x * P z
neg :
  Eq (α := PointClass F) ⟦W.add 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]⟧
neg₁ :
  Eq (α := PointClass F)
    ⟦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.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]⟧
⊢ 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 neg₂ : Eq (α := PointClass F)
  ⟦![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.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 [addMap_eq, add_of_X_ne hP hQ hPz hQz hx, smul_eq _ <| isUnit_addZ_of_X_ne hP hQ hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : PointClass F
hP : W.NonsingularLift P
hQ : W.NonsingularLift Q
⊢ W.NonsingularLift (W.addMap P Q)
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.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a) Q)
Tactic: rcases P
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 Q : PointClass F
hQ : W.NonsingularLift Q
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.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a) Q)
have mk : ∀ (a_1 : Fin 3 → F)
  (hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1)),
  W.NonsingularLift
    (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)
      (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1))
Tactic: rcases Q
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
hP : ¬W.Nonsingular P
⊢ Eq (α := W.toAffine.Point) (toAffine W P) 0
have rw : Eq.{u + 1} (α := W.toAffine.Point)
  (if hP : W.Nonsingular P ∧ P z ≠ 0 then Affine.Point.some (P x / P z) (P y / P z) sorry else 0) 0
Tactic: rw [toAffine, dif_neg <| not_and_of_not_left _ hP]
-- 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
rw :
  Eq.{u + 1} (α := W.toAffine.Point)
    (if hP : W.Nonsingular P ∧ P z ≠ 0 then Affine.Point.some (P x / P z) (P y / P z) ⋯ else 0) 0
⊢ Eq (α := W.toAffine.Point) (toAffine W P) 0
have rw₁ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [toAffine, dif_neg <| not_and_of_not_left _ hP]
-- 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 (α := W.toAffine.Point) (toAffine W P) 0
have rw : Eq.{u + 1} (α := W.toAffine.Point)
  (if hP : W.Nonsingular P ∧ P z ≠ 0 then Affine.Point.some (P x / P z) (P y / P z) sorry else 0) 0
Tactic: rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => 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.{u + 1} (α := W.toAffine.Point)
    (if hP : W.Nonsingular P ∧ P z ≠ 0 then Affine.Point.some (P x / P z) (P y / P z) ⋯ else 0) 0
⊢ Eq (α := W.toAffine.Point) (toAffine W P) 0
have rw₁ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => 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
hP : W.Nonsingular P
hPz : P z ≠ 0
⊢ toAffine W P = Affine.Point.some (P x / P z) (P y / P z) ⋯
have rw : (if hP : W.Nonsingular P ∧ P z ≠ 0 then Affine.Point.some (P x / P z) (P y / P z) sorry else 0) =
  Affine.Point.some (P x / P z) (P y / P z) sorry
Tactic: rw [toAffine, dif_pos ⟨hP, 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
hP : W.Nonsingular P
hPz : P z ≠ 0
rw :
  (if hP : W.Nonsingular P ∧ P z ≠ 0 then Affine.Point.some (P x / P z) (P y / P z) ⋯ else 0) =
    Affine.Point.some (P x / P z) (P y / P z) ⋯
⊢ toAffine W P = Affine.Point.some (P x / P z) (P y / P z) ⋯
have rw₁ : Affine.Point.some (P x / P z) (P y / P z) sorry = Affine.Point.some (P x / P z) (P y / P z) sorry
Tactic: rw [toAffine, dif_pos ⟨hP, 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
u : F
hu : IsUnit u
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have pos : ∀ (hP : W.Nonsingular P), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
Tactic: by_cases hP : W.Nonsingular P
-- 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
u : F
hu : IsUnit u
pos : ∀ (hP : W.Nonsingular P), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg : ∀ (hP : ¬W.Nonsingular P), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
Tactic: by_cases hP : W.Nonsingular P
-- 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have pos : ∀ (hPz : P z = 0), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
pos : ∀ (hPz : P z = 0), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg : ∀ (hPz : ¬P z = 0), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have pos : Eq (α := W.toAffine.Point) 0 (toAffine W P)
Tactic: rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
pos : Eq (α := W.toAffine.Point) 0 (toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have pos₁ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg : (u • P) x / (u • P) z = P x / P z ∧ (u • P) y / (u • P) z = P y / P z
Tactic: rw [toAffine_of_Z_ne_zero ((nonsingular_smul P hu).mpr hP) <| mul_ne_zero hu.ne_zero hPz,
        toAffine_of_Z_ne_zero hP hPz, Affine.Point.some.injEq]
-- 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
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg : Eq (α := W.toAffine.Point) 0 (toAffine W P)
Tactic: rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]
-- 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
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
neg : Eq (α := W.toAffine.Point) 0 (toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg₁ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]
-- 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
h : P ≈ Q
⊢ Eq (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have rcases : ∀ (u : Fˣ), Eq (α := W.toAffine.Point) (toAffine W ((fun (m : Fˣ) ↦ m • Q) u)) (toAffine W 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
hP : W.Nonsingular P
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos : ∀ (hPz : P z = 0), Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W 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), Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg : ∀ (hPz : ¬P z = 0), Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W 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
hPz : P z = 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos : Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-P y) ![0, 1, 0]))
  (-toAffine W P)
Tactic: rw [neg_of_Z_eq_zero hP.left hPz, toAffine_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]
-- 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
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-P y) ![0, 1, 0]))
    (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) (-toAffine W P)
Tactic: rw [neg_of_Z_eq_zero hP.left hPz, toAffine_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]
-- 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
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-P y) ![0, 1, 0]))
    (-toAffine W P)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos₂ : Eq (α := W.toAffine.Point) 0 (-toAffine W P)
Tactic: rw [neg_of_Z_eq_zero hP.left hPz, toAffine_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]
-- 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
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-P y) ![0, 1, 0]))
    (-toAffine W P)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) (-toAffine W P)
pos₂ : Eq (α := W.toAffine.Point) 0 (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 (-0)
Tactic: rw [neg_of_Z_eq_zero hP.left hPz, toAffine_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]
-- 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
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-P y) ![0, 1, 0]))
    (-toAffine W P)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) (-toAffine W P)
pos₂ : Eq (α := W.toAffine.Point) 0 (-toAffine W P)
pos₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 (-0)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos₄ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [neg_of_Z_eq_zero hP.left hPz, toAffine_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]