-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_addZ (P Q : Fin 3 → R) :
    (W'.map f).toProjective.addZ (f ∘ P) (f ∘ Q) = f (W'.addZ 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.addZ (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addZ P Q)

Tactic:
simp only [addZ]

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) z + 3 * (⇑f ∘ P) x * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z +
                        (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) z ^ 2 -
                      (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 2 +
                    (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 -
                (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 +
            (map W' f).toProjective.a₃ * (⇑f ∘ P) y * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 -
          (map W' f).toProjective.a₃ * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z -
        (map W' f).toProjective.a₄ * (⇑f ∘ P) x * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 +
      (map W' f).toProjective.a₄ * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z =
    f
      (-3 * P x ^ 2 * Q x * Q z + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * P z ^ 2 +
                      W'.a₁ * P x * P y * Q z ^ 2 -
                    W'.a₁ * Q x * Q y * P z ^ 2 -
                  W'.a₂ * P x ^ 2 * Q z ^ 2 +
                W'.a₂ * Q x ^ 2 * P z ^ 2 +
              W'.a₃ * P y * P z * Q z ^ 2 -
            W'.a₃ * Q y * P z ^ 2 * Q z -
          W'.a₄ * P x * P z * Q z ^ 2 +
        W'.a₄ * Q x * 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) z + 3 * (⇑f ∘ P) x * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z +
                        (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) z ^ 2 -
                      (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 2 +
                    (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 -
                (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 +
            (map W' f).toProjective.a₃ * (⇑f ∘ P) y * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 -
          (map W' f).toProjective.a₃ * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z -
        (map W' f).toProjective.a₄ * (⇑f ∘ P) x * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 +
      (map W' f).toProjective.a₄ * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z =
    f
      (-3 * P x ^ 2 * Q x * Q z + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * P z ^ 2 +
                      W'.a₁ * P x * P y * Q z ^ 2 -
                    W'.a₁ * Q x * Q y * P z ^ 2 -
                  W'.a₂ * P x ^ 2 * Q z ^ 2 +
                W'.a₂ * Q x ^ 2 * P z ^ 2 +
              W'.a₃ * P y * P z * Q z ^ 2 -
            W'.a₃ * Q y * P z ^ 2 * Q z -
          W'.a₄ * P x * P z * Q z ^ 2 +
        W'.a₄ * Q x * P z ^ 2 * Q z)

Tactic:
map_simp

Result:
no goals