-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
simp_rw :
  (p * 1 + q * 0) *
        ((q *
              HAdd.hAdd (β := R[X])
                (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₆ : R[X]) *
            if Eq (α := Fin 2) 0 1 then 1 else 0) +
          (p -
              q *
                HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W'.a₃ : R[X])) *
            1) -
      (q *
              HAdd.hAdd (β := R[X])
                (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₆ : R[X]) *
            1 +
          (p -
              q *
                HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W'.a₃ : R[X])) *
            0) *
        ((p * if Eq (α := Fin 2) 0 1 then 1 else 0) + q * 1) =
    HPow.hPow (β := ℕ) p 2 -
        p * q *
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
      HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])
⊢ (Algebra.norm R[X] : (a : W'.CoordinateRing) → R[X])
      (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)) =
    HPow.hPow (β := ℕ) p 2 -
        p * q *
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
      HPow.hPow (β := ℕ) q 2 *
        HAdd.hAdd (β := R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
          ((C : (a : R) → R[X]) W'.a₆ : R[X])

Tactic:
simp_rw [Algebra.norm_eq_matrix_det <| CoordinateRing.basis W', Matrix.det_fin_two,
    Algebra.leftMulMatrix_eq_repr_mul, basis_zero, mul_one, basis_one, smul_basis_mul_Y, map_add,
    Finsupp.add_apply, map_smul, Finsupp.smul_apply, ← basis_zero, ← basis_one,
    Basis.repr_self_apply, if_pos, one_ne_zero, if_false, smul_eq_mul]

Premises used: WeierstrassCurve.Affine.CoordinateRing.basis_one, Algebra.norm_eq_matrix_det, Module.Basis.repr_self_apply, if_false, Finsupp.add_apply, map_add, if_pos, Finsupp.smul_apply, WeierstrassCurve.Affine.CoordinateRing.basis, WeierstrassCurve.Affine.CoordinateRing.basis_zero, smul_eq_mul, mul_one, Matrix.det_fin_two, one_ne_zero, Algebra.leftMulMatrix_eq_repr_mul, map_smul, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y