-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
f : R[M]
hM :
  ∀ (m : M),
    ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
      Eq (α := R[M])
        (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
                MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
              (a : MvPolynomial (↑S : Type u_2) R) → R[M])
            a :
          R[M])
        ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])
hadd :
  ∀ (f g : R[M])
    (ihf :
      ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
        ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
                MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
              (a : MvPolynomial (↑S : Type u_2) R) → R[M])
            a =
          f)
    (ihg :
      ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
        ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
                MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
              (a : MvPolynomial (↑S : Type u_2) R) → R[M])
            a =
          g),
    ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
      ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          a =
        f + g
hsmul :
  ∀ (r : R) (f : R[M])
    (ih :
      ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
        ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
                MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
              (a : MvPolynomial (↑S : Type u_2) R) → R[M])
            a =
          f),
    ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
      ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          a =
        r • f
⊢ ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    ((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
          (a : MvPolynomial (↑S : Type u_2) R) → R[M])
        a =
      f

Tactic:
induction f using induction_on with
  | hM m =>
    have : m ∈ closure S := hS.symm ▸ mem_top _
    refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]; rfl⟩
  | hadd f g ihf ihg =>
    rcases ihf with ⟨P, rfl⟩
    rcases ihg with ⟨Q, rfl⟩
    exact ⟨P + Q, map_add _ _ _⟩
  | hsmul r f ih =>
    rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

Premises used: AddMonoidAlgebra.induction_on, rfl