-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma smul_basis_mul_Y (p q : R[X]) : (p • (1 : W.CoordinateRing) + q • mk W Y) * mk W Y =
    (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) • (1 : W.CoordinateRing) +
      (p - q * (C W.a₁ * X + C W.a₃)) • mk W Y

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
Y_sq : (mk W) Y ^ 2 = (mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y)
⊢ (mk W) (C p) * (1 * (mk W) Y) +
      (mk W) (C q) *
        ((mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) - (mk W) (C (C W.a₁ * X + C W.a₃)) * (mk W) Y) =
    (mk W) (C q) * ((mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) * 1) +
      ((mk W) (C p) - (mk W) (C q) * (mk W) (C (C W.a₁ * X + C W.a₃))) * (mk W) Y

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ (p • 1 + q • (mk W) Y) * (mk W) Y =
    (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) • 1 + (p - q * (C W.a₁ * X + C W.a₃)) • (mk W) Y

Tactic:
have Y_sq : mk W Y ^ 2 =
    mk W (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y) := by
  exact AdjoinRoot.mk_eq_mk.mpr ⟨1, by rw [polynomial]; ring1⟩

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
Y_sq : (mk W) Y ^ 2 = (mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y)
⊢ (p • 1 + q • (mk W) Y) * (mk W) Y =
    (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) • 1 + (p - q * (C W.a₁ * X + C W.a₃)) • (mk W) Y

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ (mk W) Y ^ 2 = (mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y)

Tactic:
exact AdjoinRoot.mk_eq_mk.mpr ⟨1, by rw [polynomial]; ring1⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ (fun x => x ^ 2) Y - (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y) =
    W.polynomial * 1

Tactic:
rw [polynomial]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ (fun x => x ^ 2) Y - (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y) =
    (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) * 1

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
Y_sq : (mk W) Y ^ 2 = (mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y)
⊢ (p • 1 + q • (mk W) Y) * (mk W) Y =
    (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) • 1 + (p - q * (C W.a₁ * X + C W.a₃)) • (mk W) Y

Tactic:
simp only [smul, add_mul, mul_assoc, ← sq, Y_sq, C_sub, map_sub, C_mul, _root_.map_mul]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
Y_sq : (mk W) Y ^ 2 = (mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y)
⊢ (mk W) (C p) * (1 * (mk W) Y) +
      (mk W) (C q) *
        ((mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) - (mk W) (C (C W.a₁ * X + C W.a₃)) * (mk W) Y) =
    (mk W) (C q) * ((mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) * 1) +
      ((mk W) (C p) - (mk W) (C q) * (mk W) (C (C W.a₁ * X + C W.a₃))) * (mk W) Y

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ (fun x => x ^ 2) Y - (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y) =
    (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) * 1

Tactic:
ring1

Result:
no goals