awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)

Tactic:
simpa only [add_of_Z_eq_zero_left hP.left hPz hQz,
        nonsingular_smul _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]

Premises used: Ne.isUnit, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, WeierstrassCurve.Projective.add_of_Z_eq_zero_left, IsUnit.mul, IsUnit.pow, And.left, OfNat.ofNat, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
neg : ∀ (hQz : ¬Q z = 0), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hQz : Q z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)

Tactic:
simpa only [add_of_Z_eq_zero_right hQ.left hPz hQz,
        nonsingular_smul _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]

Premises used: Ne.isUnit, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, IsUnit.mul, IsUnit.pow, WeierstrassCurve.Projective.add_of_Z_eq_zero_right, And.left, IsUnit.neg, OfNat.ofNat, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
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)
⊢ 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

Premises used: WeierstrassCurve.Projective.negY, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
neg : ∀ (hy : ¬P y * Q z = Q y * P z), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hy : P y * Q z = Q y * P z

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
hy : P y * Q z = Q y * P z
⊢ W.Nonsingular (W.add P Q)

Tactic:
simp only [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
              isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]

Premises used: WeierstrassCurve.Projective.isUnit_dblU_of_Y_eq, And.right, And.left, WeierstrassCurve.Projective.add_of_Y_eq, WeierstrassCurve.Projective.nonsingular_zero, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
hy : ¬P y * Q z = Q y * P z
⊢ W.Nonsingular (W.add P Q)

Tactic:
simp only [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            nonsingular_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, nonsingular_zero]

Premises used: WeierstrassCurve.Projective.isUnit_addU_of_Y_ne, And.left, WeierstrassCurve.Projective.nonsingular_zero, WeierstrassCurve.Projective.add_of_Y_ne, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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.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
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
neg : ∀ (hx : ¬P x * Q z = Q x * P z), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hx : P x * Q z = Q x * P z

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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]
hx : P x * Q z = Q x * P z
⊢ W.Nonsingular (W.add P Q)

Tactic:
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]

Premises used: WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne', And.left, WeierstrassCurve.Projective.add_of_Y_ne', Iff.mp, not_and, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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]
hx : ¬P x * Q z = Q x * P z
⊢ W.Nonsingular (W.add P Q)

Tactic:
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]

Premises used: And.left, WeierstrassCurve.Projective.add_of_X_ne, WeierstrassCurve.Projective.isUnit_addZ_of_X_ne, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
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])
    (hx : ¬P x * Q z = Q x * P z), W.Nonsingular (W.add P Q)
⊢ 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]

Premises used: OfNat.ofNat, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
⊢ Eq (α := PointClass R) (W'.addMap ⟦P⟧ ⟦Q⟧) ⟦W'.add P Q⟧

Tactic:
rfl

Premises used: Quotient.map₂, WeierstrassCurve.Projective.addMap, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
revert : ∀ (hQ : W.NonsingularLift Q), W.addMap ⟦P⟧ Q = Q
⊢ W.addMap ⟦P⟧ Q = Q

Tactic:
revert hQ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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

Tactic:
Q.inductionOn (motive := fun Q => _ → W.addMap _ Q = Q) fun Q hQ => ?_

Premises used: Quotient.inductionOn
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
refine : ∀ (Q : Fin 3 → F) (hQ : W.NonsingularLift ⟦Q⟧), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
⊢ ∀ (hQ : W.NonsingularLift Q), W.addMap ⟦P⟧ Q = Q

Tactic:
refine Q.inductionOn (motive := fun Q => _ → W.addMap _ Q = Q) fun Q hQ => ?_

Premises used: Quotient.inductionOn
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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⟧
neg : ∀ (hQz : ¬Q z = 0), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦Q⟧

Tactic:
by_cases hQz : Q z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
pos : (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![0, 1, 0] Q
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦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]

Premises used: WeierstrassCurve.Projective.add_of_Z_eq_zero, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.addMap_eq, IsUnit.pow, OfNat.ofNat, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![0, 1, 0] Q

Tactic:
Setoid.symm <| equiv_zero_of_Z_eq_zero hQ hQz

Premises used: Setoid.symm, WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![0, 1, 0] Q

Tactic:
exact Setoid.symm <| equiv_zero_of_Z_eq_zero hQ hQz

Premises used: Setoid.symm, WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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⟧
neg₂ neg₃ : Eq (α := PointClass F) ⟦Q⟧ ⟦Q⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦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]

Premises used: Ne.isUnit, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.add_of_Z_eq_zero_left, IsUnit.mul, WeierstrassCurve.Projective.addMap_eq, IsUnit.pow, And.left, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
revert : ∀ (hP : W.NonsingularLift P), W.addMap P ⟦Q⟧ = P
⊢ W.addMap P ⟦Q⟧ = P

Tactic:
revert hP
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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

Tactic:
P.inductionOn (motive := fun P => _ → W.addMap P _ = P) fun P hP => ?_

Premises used: Quotient.inductionOn
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
refine : ∀ (P : Fin 3 → F) (hP : W.NonsingularLift ⟦P⟧), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
⊢ ∀ (hP : W.NonsingularLift P), W.addMap P ⟦Q⟧ = P

Tactic:
refine P.inductionOn (motive := fun P => _ → W.addMap P _ = P) fun P hP => ?_

Premises used: Quotient.inductionOn
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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⟧
neg : ∀ (hPz : ¬P z = 0), Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧

Tactic:
by_cases hPz : P z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
pos : (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![0, 1, 0] P
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦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]

Premises used: WeierstrassCurve.Projective.add_of_Z_eq_zero, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.addMap_eq, IsUnit.pow, OfNat.ofNat, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![0, 1, 0] P

Tactic:
Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

Premises used: Setoid.symm, WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![0, 1, 0] P

Tactic:
exact Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

Premises used: Setoid.symm, WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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⟧
neg₂ neg₃ : Eq (α := PointClass F) ⟦P⟧ ⟦P⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦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]

Premises used: Ne.isUnit, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, WeierstrassCurve.Projective.smul_eq, IsUnit.mul, WeierstrassCurve.Projective.addMap_eq, IsUnit.pow, WeierstrassCurve.Projective.add_of_Z_eq_zero_right, And.left, IsUnit.neg, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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]⟧
neg : ∀ (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]⟧

Tactic:
by_cases hy : P y * Q z = Q y * P z

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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]⟧
pos₂ pos₃ : Eq.{u + 1} (α := PointClass F) ⟦![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦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']

Premises used: WeierstrassCurve.Projective.isUnit_dblU_of_Y_eq, WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.addMap_eq, And.left, WeierstrassCurve.Projective.add_of_Y_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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]⟧
neg₂ neg₃ : Eq.{u + 1} (α := PointClass F) ⟦![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦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]

Premises used: WeierstrassCurve.Projective.isUnit_addU_of_Y_ne, WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.addMap_eq, And.left, WeierstrassCurve.Projective.add_of_Y_ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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]⟧
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]⟧
⊢ 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

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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]⟧
pos₂ 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]⟧
⊢ 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:
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]

Premises used: WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.addMap_eq, WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne', WeierstrassCurve.Projective.add_of_Y_ne', Iff.mp, not_and