-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.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 ^ 2 = Q x * P z ^ 2)
    (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
    W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) =
      -W.dblU P / W.dblZ P

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
hPy : P y - W.negY P ≠ 0
⊢ (toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ 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 : Jacobian 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 ^ 2 = Q x / Q z ^ 2
hy : ¬P y / P z ^ 3 = (toAffine W).negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)
⊢ (toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x / Q z ^ 2
hy : ¬P y / P z ^ 3 = (toAffine W).negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)
⊢ (toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P

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

Result:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x / Q z ^ 2
hy : ¬P y / P z ^ 3 = (toAffine W).negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)
⊢ (3 * (P x / P z ^ 2) ^ 2 + 2 * (toAffine W).a₂ * (P x / P z ^ 2) + (toAffine W).a₄ -
        (toAffine W).a₁ * (P y / P z ^ 3)) /
      (P y / P z ^ 3 - W.negY P / P z ^ 3) =
    -(W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4)) / (P z * (P y - W.negY P))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x / Q z ^ 2
hy : ¬P y / P z ^ 3 = (toAffine W).negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)
⊢ (3 * (P x / P z ^ 2) ^ 2 + 2 * (toAffine W).a₂ * (P x / P z ^ 2) + (toAffine W).a₄ -
        (toAffine W).a₁ * (P y / P z ^ 3)) /
      (P y / P z ^ 3 - W.negY P / P z ^ 3) =
    -(W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4)) / (P z * (P y - W.negY P))

Tactic:
field_simp [pow_ne_zero 2 hPz]

Result:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x / Q z ^ 2
hy : ¬P y / P z ^ 3 = (toAffine W).negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)
⊢ ((3 * P x ^ 2 * P z ^ 2 + 2 * (toAffine W).a₂ * P x * (P z ^ 2) ^ 2 + (toAffine W).a₄ * ((P z ^ 2) ^ 2 * P z ^ 2)) *
            P z ^ 3 -
          (P z ^ 2) ^ 2 * P z ^ 2 * ((toAffine W).a₁ * P y)) *
        P z ^ 3 *
      (P z * (P y - W.negY P)) =
    (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4 - W.a₁ * P y * P z) *
      ((P z ^ 2) ^ 2 * P z ^ 2 * P z ^ 3 * (P y - W.negY P))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x / Q z ^ 2
hy : ¬P y / P z ^ 3 = (toAffine W).negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)
⊢ ((3 * P x ^ 2 * P z ^ 2 + 2 * (toAffine W).a₂ * P x * (P z ^ 2) ^ 2 + (toAffine W).a₄ * ((P z ^ 2) ^ 2 * P z ^ 2)) *
            P z ^ 3 -
          (P z ^ 2) ^ 2 * P z ^ 2 * ((toAffine W).a₁ * P y)) *
        P z ^ 3 *
      (P z * (P y - W.negY P)) =
    (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4 - W.a₁ * P y * P z) *
      ((P z ^ 2) ^ 2 * P z ^ 2 * P z ^ 3 * (P y - W.negY P))

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ (toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P

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

Result:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
hPy : P y - W.negY P ≠ 0
⊢ (toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P