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.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
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
have pos : ∀ (hy : P y * Q z = Q y * P z), Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 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
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
pos : ∀ (hy : P y * Q z = Q y * P z), Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
have neg : ∀ (hy : ¬P y * Q z = Q y * P z), Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 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
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
hy : P y * Q z = Q y * P z
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
have pos : Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0])) 0
Tactic: rw [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right,
            toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, toAffine_zero]
-- 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
hy : P y * Q z = Q y * P z
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0])) 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
have pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) 0
Tactic: rw [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right,
            toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, toAffine_zero]
-- 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
hy : P y * Q z = Q y * P z
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0])) 0
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
have pos₂ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right,
            toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, toAffine_zero]
-- 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
hy : ¬P y * Q z = Q y * P z
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
have neg : Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0])) 0
Tactic: rw [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            toAffine_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, toAffine_zero]
-- 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
hy : ¬P y * Q z = Q y * P z
neg :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0])) 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
have neg₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) 0
Tactic: rw [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            toAffine_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, toAffine_zero]
-- 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
hy : ¬P y * Q z = Q y * P z
neg :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0])) 0
neg₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
have neg₂ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            toAffine_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, toAffine_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (hypothesis)
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)
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have this : toAffine W
    ![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] =
  HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: have := toAffine_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
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)
this :
  toAffine W
      ![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] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have pos : ∀ (hx : P x * Q z = Q x * P z), toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W 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
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)
this :
  toAffine W
      ![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] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
pos :
  ∀ (hx : P x * Q z = Q x * P z),
    toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have neg : ∀ (hx : ¬P x * Q z = Q x * P z),
  toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W 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
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)
this :
  toAffine W
      ![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] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
hx : P x * Q z = Q x * P z
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have pos : toAffine W
    (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]) =
  HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: rwa [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            toAffine_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left 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.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 :
  toAffine W
      ![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] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
hx : ¬P x * Q z = Q x * P z
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have neg : toAffine W
    (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]) =
  HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: rwa [add_of_X_ne hP.left hQ.left hPz hQz hx,
            toAffine_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 : W.Point
⊢ (-P).toAffineLift = -P.toAffineLift
have mk : ∀ {point : PointClass F} (a : Fin 3 → F)
  (hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)),
  (-{ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point }).toAffineLift =
    -{ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a,
          nonsingular := hP }.toAffineLift
Tactic: rcases P with @⟨⟨_⟩, hP⟩
Cleared hypotheses: P
-- 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 : W.Point
⊢ (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift
have mk : ∀ {point : PointClass F} (a : Fin 3 → F)
  (hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a))
  {point : PointClass F} (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)),
  ({ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point } +
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }).toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point }.toAffineLift +
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }.toAffineLift
Tactic: rcases P, Q with ⟨@⟨⟨_⟩, hP⟩, @⟨⟨_⟩, hQ⟩⟩
Cleared hypotheses: P, Q
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }
have pos : ∀ (hPz : P z = 0),
  fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }
Tactic: by_cases hPz : P z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
pos :
  ∀ (hPz : P z = 0),
    fromAffine
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
            nonsingular := hP : W.Point }.toAffineLift =
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
        nonsingular := hP }
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }
have neg : ∀ (hPz : ¬P z = 0),
  fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }
Tactic: by_cases hPz : P z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : P z = 0
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }
have pos : Point.point (W' := W) (fromAffine 0) =
  { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
      W.Point }.point
Tactic: rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_eq_zero hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : ¬P z = 0
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }
have neg : (fromAffine (Affine.Point.some (P x / P z) (P y / P z) sorry)).point =
  { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
      W.Point }.point
Tactic: rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_ne_zero hP hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine Affine.Point.zero)) Affine.Point.zero
have zero : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine 0)) 0
Tactic: rw [← Affine.Point.zero_def, fromAffine_zero, toAffineLift_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
zero : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine 0)) 0
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine Affine.Point.zero)) Affine.Point.zero
have zero₁ : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift 0) 0
Tactic: rw [← Affine.Point.zero_def, fromAffine_zero, toAffineLift_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
zero : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine 0)) 0
zero₁ : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift 0) 0
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine Affine.Point.zero)) Affine.Point.zero
have zero₂ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [← Affine.Point.zero_def, fromAffine_zero, toAffineLift_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
x y : F
h : W.toAffine.Nonsingular «x» «y»
⊢ (fromAffine (Affine.Point.some «x» «y» h)).toAffineLift = Affine.Point.some «x» «y» h
have some : { point := ⟦![«x», «y», 1]⟧, nonsingular := sorry : W.Point }.toAffineLift = Affine.Point.some «x» «y» h
Tactic: rw [fromAffine_some, toAffineLift_some]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
x y : F
h : W.toAffine.Nonsingular «x» «y»
some : { point := ⟦![«x», «y», 1]⟧, nonsingular := ⋯ : W.Point }.toAffineLift = Affine.Point.some «x» «y» h
⊢ (fromAffine (Affine.Point.some «x» «y» h)).toAffineLift = Affine.Point.some «x» «y» h
have some₁ : Affine.Point.some «x» «y» sorry = Affine.Point.some «x» «y» h
Tactic: rw [fromAffine_some, toAffineLift_some]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
x x_1 x_2 : W.Point
⊢ «x» + x_1 + x_2 = «x» + (x_1 + x_2)
have a : Eq (α := W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1 + x_2) : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + (x_1 + x_2)) : W.toAffine.Point)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
x x_1 x_2 : W.Point
⊢ «x» + x_1 + x_2 = «x» + (x_1 + x_2)
have a : Eq (α := W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1 + x_2) : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + (x_1 + x_2)) : W.toAffine.Point)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
x : W.Point
⊢ 0 + «x» = «x»
have a : Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (0 + «x») : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
x : W.Point
⊢ 0 + «x» = «x»
have a : Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (0 + «x») : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, zero_add]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
x : W.Point
⊢ «x» + 0 = «x»
have a : Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + 0) : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
x : W.Point
⊢ «x» + 0 = «x»
have a : Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + 0) : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]