-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma equation_smul (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.Equation (u • P) ↔ W'.Equation P :=
  have hP (u : R) {P : Fin 3 → R} (hP : W'.Equation P) : W'.Equation <| u • P

Proof state:
case h.e'_4
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ P = ↑hu.unit⁻¹ • u • P

Tactic:
rw [smul_smul, hu.val_inv_mul, one_smul]

Result:
no goals

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
    0
⊢ (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y * (u • P) z + W'.a₃ * (u • P) y * (u • P) z ^ 3 -
          ((u • P) x ^ 3 + W'.a₂ * (u • P) x ^ 2 * (u • P) z ^ 2 + W'.a₄ * (u • P) x * (u • P) z ^ 4 +
            W'.a₆ * (u • P) z ^ 6) +
        u ^ 6 * 0 -
      (0 +
        u ^ 6 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
simp only [smul_fin3_ext]

Result:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
    0
⊢ (u ^ 3 * P y) ^ 2 + W'.a₁ * (u ^ 2 * P x) * (u ^ 3 * P y) * (u * P z) + W'.a₃ * (u ^ 3 * P y) * (u * P z) ^ 3 -
          ((u ^ 2 * P x) ^ 3 + W'.a₂ * (u ^ 2 * P x) ^ 2 * (u * P z) ^ 2 + W'.a₄ * (u ^ 2 * P x) * (u * P z) ^ 4 +
            W'.a₆ * (u * P z) ^ 6) +
        u ^ 6 * 0 -
      (0 +
        u ^ 6 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
    0
⊢ (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y * (u • P) z + W'.a₃ * (u • P) y * (u • P) z ^ 3 -
      ((u • P) x ^ 3 + W'.a₂ * (u • P) x ^ 2 * (u • P) z ^ 2 + W'.a₄ * (u • P) x * (u • P) z ^ 4 +
        W'.a₆ * (u • P) z ^ 6) =
    0

Tactic:
linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) u ^ 6 * hP

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.Equation (u • P)

Tactic:
rw [equation_iff] at hP ⊢

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
    0
⊢ (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y * (u • P) z + W'.a₃ * (u • P) y * (u • P) z ^ 3 -
      ((u • P) x ^ 3 + W'.a₂ * (u • P) x ^ 2 * (u • P) z ^ 2 + W'.a₄ * (u • P) x * (u • P) z ^ 4 +
        W'.a₆ * (u • P) z ^ 6) =
    0

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
    0
⊢ (u ^ 3 * P y) ^ 2 + W'.a₁ * (u ^ 2 * P x) * (u ^ 3 * P y) * (u * P z) + W'.a₃ * (u ^ 3 * P y) * (u * P z) ^ 3 -
          ((u ^ 2 * P x) ^ 3 + W'.a₂ * (u ^ 2 * P x) ^ 2 * (u * P z) ^ 2 + W'.a₄ * (u ^ 2 * P x) * (u * P z) ^ 4 +
            W'.a₆ * (u * P z) ^ 6) +
        u ^ 6 * 0 -
      (0 +
        u ^ 6 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ W'.Equation P

Tactic:
convert hP ↑hu.unit⁻¹ h

Result:
case h.e'_4
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ P = ↑hu.unit⁻¹ • u • P