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

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

Tactic:
simp only [negAddY]

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

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

Tactic:
map_simp

Result:
no goals