-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_negAddY (P Q : Fin 3 → R) :
    (W'.map f).toJacobian.negAddY (f ∘ P) (f ∘ Q) = f (W'.negAddY P Q)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ (map W' f).toJacobian.negAddY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.negAddY P Q)

Tactic:
simp only [negAddY]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ -(⇑f ∘ P) y * (⇑f ∘ Q) x ^ 3 * (⇑f ∘ P) z ^ 3 + 2 * (⇑f ∘ P) y * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 3 -
                                        3 * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z +
                                      3 * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 +
                                    (⇑f ∘ P) x ^ 3 * (⇑f ∘ Q) y * (⇑f ∘ Q) z ^ 3 -
                                  2 * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) y * (⇑f ∘ Q) z ^ 3 +
                                (map W' f).toJacobian.a₁ * (⇑f ∘ P) x * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 4 +
                              (map W' f).toJacobian.a₁ * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 3 *
                                (⇑f ∘ Q) z -
                            (map W' f).toJacobian.a₁ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ P) z *
                              (⇑f ∘ Q) z ^ 3 -
                          (map W' f).toJacobian.a₁ * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) z ^ 4 -
                        2 * (map W' f).toJacobian.a₂ * (⇑f ∘ P) x * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 4 *
                          (⇑f ∘ Q) z +
                      2 * (map W' f).toJacobian.a₂ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ P) z *
                        (⇑f ∘ Q) z ^ 4 +
                    (map W' f).toJacobian.a₃ * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 6 -
                  (map W' f).toJacobian.a₃ * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) z ^ 6 -
                (map W' f).toJacobian.a₄ * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 6 * (⇑f ∘ Q) z -
              (map W' f).toJacobian.a₄ * (⇑f ∘ P) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 4 * (⇑f ∘ Q) z ^ 3 +
            (map W' f).toJacobian.a₄ * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 3 * (⇑f ∘ Q) z ^ 4 +
          (map W' f).toJacobian.a₄ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 6 -
        2 * (map W' f).toJacobian.a₆ * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 6 * (⇑f ∘ Q) z ^ 3 +
      2 * (map W' f).toJacobian.a₆ * (⇑f ∘ P) y * (⇑f ∘ P) z ^ 3 * (⇑f ∘ Q) z ^ 6 =
    f
      (-P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z +
                                        3 * P x * P y * Q x ^ 2 * P z * Q z ^ 2 +
                                      P x ^ 3 * Q y * Q z ^ 3 -
                                    2 * P y ^ 2 * Q y * Q z ^ 3 +
                                  W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                              W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                            W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                          2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                        2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                      W'.a₃ * Q y ^ 2 * P z ^ 6 -
                    W'.a₃ * P y ^ 2 * Q z ^ 6 -
                  W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
              W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
            W'.a₄ * P x * P y * P z * Q z ^ 6 -
          2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
        2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ -(⇑f ∘ P) y * (⇑f ∘ Q) x ^ 3 * (⇑f ∘ P) z ^ 3 + 2 * (⇑f ∘ P) y * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 3 -
                                        3 * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z +
                                      3 * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 +
                                    (⇑f ∘ P) x ^ 3 * (⇑f ∘ Q) y * (⇑f ∘ Q) z ^ 3 -
                                  2 * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) y * (⇑f ∘ Q) z ^ 3 +
                                (map W' f).toJacobian.a₁ * (⇑f ∘ P) x * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 4 +
                              (map W' f).toJacobian.a₁ * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 3 *
                                (⇑f ∘ Q) z -
                            (map W' f).toJacobian.a₁ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ P) z *
                              (⇑f ∘ Q) z ^ 3 -
                          (map W' f).toJacobian.a₁ * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) z ^ 4 -
                        2 * (map W' f).toJacobian.a₂ * (⇑f ∘ P) x * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 4 *
                          (⇑f ∘ Q) z +
                      2 * (map W' f).toJacobian.a₂ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ P) z *
                        (⇑f ∘ Q) z ^ 4 +
                    (map W' f).toJacobian.a₃ * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 6 -
                  (map W' f).toJacobian.a₃ * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) z ^ 6 -
                (map W' f).toJacobian.a₄ * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 6 * (⇑f ∘ Q) z -
              (map W' f).toJacobian.a₄ * (⇑f ∘ P) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 4 * (⇑f ∘ Q) z ^ 3 +
            (map W' f).toJacobian.a₄ * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 3 * (⇑f ∘ Q) z ^ 4 +
          (map W' f).toJacobian.a₄ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 6 -
        2 * (map W' f).toJacobian.a₆ * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 6 * (⇑f ∘ Q) z ^ 3 +
      2 * (map W' f).toJacobian.a₆ * (⇑f ∘ P) y * (⇑f ∘ P) z ^ 3 * (⇑f ∘ Q) z ^ 6 =
    f
      (-P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z +
                                        3 * P x * P y * Q x ^ 2 * P z * Q z ^ 2 +
                                      P x ^ 3 * Q y * Q z ^ 3 -
                                    2 * P y ^ 2 * Q y * Q z ^ 3 +
                                  W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                              W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                            W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                          2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                        2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                      W'.a₃ * Q y ^ 2 * P z ^ 6 -
                    W'.a₃ * P y ^ 2 * Q z ^ 6 -
                  W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
              W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
            W'.a₄ * P x * P y * P z * Q z ^ 6 -
          2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
        2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6)

Tactic:
map_simp

Result:
no goals