-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffine_add {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
    toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
have := toAffine_add_of_Z_ne_zero hP hQ hPz hQz hxy

Result:
case neg
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  toAffine W
      ![(Jacobian.toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((Jacobian.toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (Jacobian.toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((Jacobian.toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
by_cases hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

case neg
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
rw [toAffine_of_Z_ne_zero hP hPz, toAffine_of_Z_ne_zero hQ hQz, Affine.Point.add_of_Y_eq
    ((X_eq_iff hPz hQz).mp hxy.left) ((Y_eq_iff' hPz hQz).mp hxy.right)]

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ toAffine W (W.add P Q) = 0

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : ¬Q z = 0
⊢ toAffine W (W.add P Q) = toAffine W Q

Tactic:
rw [add_of_Z_eq_zero_left hP.left hPz hQz,
  toAffine_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]

Result:
no goals

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  toAffine W
      ![(Jacobian.toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((Jacobian.toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (Jacobian.toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((Jacobian.toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ toAffine W (W.add P Q) = 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 hx <| not_and.mp hxy hx]

Result:
no goals