-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid 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 : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      Eq (α := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            a :
          R[M])
        ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])
hM₁ :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) 0) : R[M])
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    Eq (α := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → 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 : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      Eq (α := R[M])
        (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
            a :
          R[M])
        ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) x) : R[M])) →
    (∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
        Eq (α := R[M])
          (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                  fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
                (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
              a :
            R[M])
          ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) y) : R[M])) →
      ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
        Eq (α := R[M])
          (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
                  fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
                (a : FreeAlgebra R (↑S : Type u_2)) → 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