-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
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) ⊤
m : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m
hM :
  ∀ (m : M) (hm : m ∈ S),
    ∃ (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])
hM₁ :
  ∃ (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) 0) : R[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])
have hM₂ : ∀ (x y : M) (hx : Membership.mem (γ := AddSubmonoid M) (closure S) x)
  (hy : Membership.mem (γ := AddSubmonoid M) (closure S) y),
  (∃ (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) x) : R[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) y) : R[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) (x + y)) :
            R[M])
Tactic: refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this