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

Tactic:
map_simp

Result:
no goals

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

Tactic:
simp only [addX]

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