-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
private lemma toAffine_slope_of_eq {P Q : Fin 3 → F} (hP : W.Equation 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) :
    W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) =
      -eval P W.polynomialX / P z / (P y - W.negY P)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation 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
⊢ (toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = -(eval P) W.polynomialX / P z / (P y - W.negY P)

Tactic:
have hPy : P y - W.negY P ≠ 0 := sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation 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
hPy : P y - W.negY P ≠ 0
⊢ (toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = -(eval P) W.polynomialX / P z / (P y - W.negY P)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hPy : P y - W.negY P ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = (toAffine W).negY (Q x / Q z) (Q y / Q z)
⊢ (3 * (P x / P z) ^ 2 + 2 * (toAffine W).a₂ * (P x / P z) + (toAffine W).a₄ - (toAffine W).a₁ * (P y / P z)) /
      (P y / P z - W.negY P / P z) =
    -(eval P) W.polynomialX / P z / (P y - W.negY P)

Tactic:
field_simp [eval_polynomialX, hPz]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hPy : P y - W.negY P ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = (toAffine W).negY (Q x / Q z) (Q y / Q z)
⊢ ((3 * P x ^ 2 * P z + 2 * (toAffine W).a₂ * P x * P z ^ 2 + (toAffine W).a₄ * (P z ^ 2 * P z)) * P z -
          P z ^ 2 * P z * ((toAffine W).a₁ * P y)) *
        P z *
      (P z * (P y - W.negY P)) =
    (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2 - W.a₁ * P y * P z) * (P z ^ 2 * P z * P z * (P y - W.negY P))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hPy : P y - W.negY P ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = (toAffine W).negY (Q x / Q z) (Q y / Q z)
⊢ (toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = -(eval P) W.polynomialX / P z / (P y - W.negY P)

Tactic:
rw [Affine.slope_of_Y_ne hx <| negY_of_Z_ne_zero hQz ▸ hy, ← negY_of_Z_ne_zero hPz]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hPy : P y - W.negY P ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = (toAffine W).negY (Q x / Q z) (Q y / Q z)
⊢ (3 * (P x / P z) ^ 2 + 2 * (toAffine W).a₂ * (P x / P z) + (toAffine W).a₄ - (toAffine W).a₁ * (P y / P z)) /
      (P y / P z - W.negY P / P z) =
    -(eval P) W.polynomialX / P z / (P y - W.negY P)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hPy : P y - W.negY P ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = (toAffine W).negY (Q x / Q z) (Q y / Q z)
⊢ ((3 * P x ^ 2 * P z + 2 * (toAffine W).a₂ * P x * P z ^ 2 + (toAffine W).a₄ * (P z ^ 2 * P z)) * P z -
          P z ^ 2 * P z * ((toAffine W).a₁ * P y)) *
        P z *
      (P z * (P y - W.negY P)) =
    (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2 - W.a₁ * P y * P z) * (P z ^ 2 * P z * P z * (P y - W.negY P))

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation 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
hPy : P y - W.negY P ≠ 0
⊢ (toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = -(eval P) W.polynomialX / P z / (P y - W.negY P)

Tactic:
simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hPy : P y - W.negY P ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = (toAffine W).negY (Q x / Q z) (Q y / Q z)
⊢ (toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = -(eval P) W.polynomialX / P z / (P y - W.negY P)