-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_add {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
    W.Nonsingular <| W.add P Q

Proof state:
case neg
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]

Result:
no goals

Proof state:
case neg
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)

Tactic:
have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy

Result:
case neg
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
    ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
        ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      1]
⊢ W.Nonsingular (W.add P Q)

Proof state:
case pos
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:
simp only [add_of_Z_eq_zero hP hQ hPz hQz,
  nonsingular_smul _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, nonsingular_zero]

Result:
no goals

Proof state:
case pos
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)

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

Result:
case pos
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)

case neg
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)

Proof state:
case pos
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
    ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
        ((toAffine W).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]

Result:
no goals

Proof state:
case neg
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
    ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
        ((toAffine W).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:
by_cases hx : P x * Q z = Q x * P z

Result:
case pos
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
    ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
        ((toAffine W).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)

case neg
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
    ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
        ((toAffine W).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)

Proof state:
case pos
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)

Tactic:
by_cases hQz : Q z = 0

Result:
case pos
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)

case neg
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)

Proof state:
case neg
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]

Result:
no goals

Proof state:
case pos
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]

Result:
no goals

Proof state:
case neg
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
    ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
        ((toAffine W).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]

Result:
no goals

Proof state:
case neg
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)

Tactic:
by_cases hQz : Q z = 0

Result:
case pos
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)

case neg
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)