-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_addX (P Q : Fin 3 → R) :
    (W'.map f).toProjective.addX (f ∘ P) (f ∘ Q) = f (W'.addX 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
⊢ -(⇑f ∘ P) x * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z + (⇑f ∘ Q) x * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) z -
                                2 * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ Q) z +
                              2 * (⇑f ∘ Q) x * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ P) 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 +
                        (map W' f).toProjective.a₂ * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) z -
                      (map W' f).toProjective.a₂ * (⇑f ∘ P) x * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z -
                    (map W' f).toProjective.a₃ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) z ^ 2 +
                  (map W' f).toProjective.a₃ * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) 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 ∘ P) x ^ 2 * (⇑f ∘ Q) z ^ 2 -
          (map W' f).toProjective.a₄ * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z ^ 2 +
        3 * (map W' f).toProjective.a₆ * (⇑f ∘ P) x * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 -
      3 * (map W' f).toProjective.a₆ * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z =
    f
      (-P x * Q y ^ 2 * P z + Q x * P y ^ 2 * Q z - 2 * P x * P y * Q y * Q z + 2 * Q x * P y * Q y * P z -
                              W'.a₁ * P x ^ 2 * Q y * Q z +
                            W'.a₁ * Q x ^ 2 * P y * P z +
                          W'.a₂ * P x ^ 2 * Q x * Q z -
                        W'.a₂ * P x * Q x ^ 2 * P z -
                      W'.a₃ * P x * P y * Q z ^ 2 +
                    W'.a₃ * Q x * Q y * P 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₄ * P x ^ 2 * Q z ^ 2 -
            W'.a₄ * Q x ^ 2 * P z ^ 2 +
          3 * W'.a₆ * P x * P z * Q z ^ 2 -
        3 * W'.a₆ * Q x * P z ^ 2 * Q z)

Tactic:
map_simp

Result:
no goals

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.addX (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)

Tactic:
simp only [addX]

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