How do I get an instance from a def?

Stream: new members

[Scott Carnahan]

I have been experimenting with a variant of Polynomial.eval, but have trouble comparing it to the existing eval:

import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Polynomial.Basic
import Mathlib.Data.Polynomial.Eval

namespace Polynomial

variable {R : Type*} [Semiring R] {S : Type*} (x : S)

/-- Scalar multiplication together with taking a natural number power. -/
def smul_pow [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] : ℕ → R → S := fun n r => r • x^n

/-- Evaluate a polynomial `p` in the scalar commutative semiring `R` at an element `x` in the target
`S` using scalar multiple `R`-action. -/
irreducible_def smeval [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (p : R[X]) : S :=
  p.sum (smul_pow x)

theorem smeval_eq_sum [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (p : R[X]) :
    p.smeval x = p.sum (smul_pow x) := by rw [smeval_def]

theorem smeval_eq_eval₂ [Semiring S] (f : R →+* S) (p : R[X]) :
    p.smeval x = p.eval₂ f x := by -- failed to synthesize instance MulActionWithZero R S
  sorry

I am clearly missing an action of R on S. A Module R S structure is defined from a ring homomorphism f in docs#RingHom.toModule but since it is not an instance, I don't know how to apply it here.

[llllvvuu]

Does haveI := RingHom.toModule f work?

[Kevin Buzzard]

Or letI? (because it's data)

[Eric Wieser]

It makes no difference here I think

[Scott Carnahan]

Thanks a lot! It ended up looking like:

theorem smeval_eq_eval₂ [Semiring S] (f : R →+* S) (p : R[X]) :
    haveI : Module R S := RingHom.toModule f -- both haveI and letI work here.
    p.smeval x = p.eval₂ f x := by
  letI : Module R S := RingHom.toModule f -- rw gets angry if I use haveI here.
  rw [smeval_eq_sum, eval₂_eq_sum]
  exact rfl