awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ⊤
r : R
f : R[M]
ih :
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((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 =
      f
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((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 • f
have hsmul : ∀ (P : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((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 =
      HSMul.hSMul (β := R[M]) r
        (((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])
            P :
          R[M])
Tactic: rcases ih with ⟨P, rfl⟩
Cleared hypotheses: f, ih
-- 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) ⊤
f : R[M]
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((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 =
      f
have hM : ∀ (m : 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])
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 ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
    · 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 _ _ _⟩
Cleared hypotheses: f
-- 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) ⊤
f : R[M]
hM :
  ∀ (m : 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])
⊢ ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((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 =
      f
have hadd : ∀ (f g : R[M])
  (ihf :
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      ((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 =
        f)
  (ihg :
    ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
      ((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 =
        g),
  ∃ (a : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)),
    ((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 =
      f + g
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 ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
    · 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 _ _ _⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
h : AddMonoid.FG M
⊢ FiniteType R R[M]
have obtain : ∀ (S : Finset M) (hS : Eq (α := AddSubmonoid M) (closure (↑S : Set M)) ⊤), FiniteType R R[M]
Tactic: obtain ⟨S, hS⟩ := h.fg_top
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
inst_2 : Nontrivial R
⊢ FiniteType R R[M] ↔ AddMonoid.FG M
have refine : ∀ (h : FiniteType R R[M]), AddMonoid.FG M
Tactic: refine ⟨fun h => ?_, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
inst_2 : Nontrivial R
h : FiniteType R R[M]
⊢ AddMonoid.FG M
have obtain : ∀ (S : Finset M) (hS : Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑S : Set M))) ⊤), AddMonoid.FG M
Tactic: obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
inst_2 : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑S : Set M))) ⊤
⊢ AddMonoid.FG M
have refine : ∀ (m : M), Membership.mem (γ := AddSubmonoid M) (closure (↑S : Set M)) m
Tactic: refine AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
inst_2 : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑S : Set M))) ⊤
m : M
⊢ Membership.mem (γ := AddSubmonoid M) (closure (↑S : Set M)) m
have hm : Membership.mem (γ := Submodule R R[M])
  ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M]) (adjoin R (of' R M '' (↑S : Set M))) :
    Submodule R R[M])
  (of' R M m)
Tactic: have hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S)) := by
    simp only [hS, top_toSubmodule, Submodule.mem_top]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
inst_2 : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑S : Set M))) ⊤
m : M
hm :
  Membership.mem (γ := Submodule R R[M])
    ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M]) (adjoin R (of' R M '' (↑S : Set M))) :
      Submodule R R[M])
    (of' R M m)
⊢ Membership.mem (γ := AddSubmonoid M) (closure (↑S : Set M)) m
have hm₁ : Membership.mem (γ := Submodule R R[M]) (span R (↑(Submonoid.closure (of' R M '' (↑S : Set M))) : Set R[M])) (of' R M m)
Tactic: rw [adjoin_eq_span] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
f : R[M]
⊢ Membership.mem (γ := Subalgebra R R[M]) (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) f
have suffices : LE.le (α := Submodule R R[M]) (span R ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M)))
  ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M])
    (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))))
Tactic: suffices span R (of R M '' f.support) ≤ Subalgebra.toSubmodule (adjoin R (of R M '' f.support)) by
    exact this (mem_span_support f)
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
f : R[M]
⊢ LE.le (α := Submodule R R[M]) (span R ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M)))
    ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M])
      (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))))
have rw : (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M) ⊆
  (↑((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M])
          (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) :
        Submodule R R[M]) :
    Set R[M])
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) ⊤
have refine : LE.le (α := Subalgebra R R[M]) ⊤ (adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M)))
Tactic: refine le_antisymm le_top ?_
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
⊢ LE.le (α := Subalgebra R R[M]) ⊤ (adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M)))
have rw : S ⊆ (↑(adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) : Set R[M])
Tactic: rw [← hS, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
f : R[M]
hf : f ∈ S
⊢ f ∈ (↑(adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) : Set R[M])
have hincl : Subset (α := Set R[M]) ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))
  (⋃ g ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑g.support : Set M))
Tactic: have hincl : (of R M '' f.support) ⊆
      ⋃ (g : R[M]) (H : g ∈ S), (of R M '' g.support) := by
    intro s hs
    exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
this :
  Eq (α := Set R[M]) (Set.image (α := M) (⇑(of R M) : (a : M) → R[M]) (⋃ f ∈ S, (↑f.support : Set M)))
    (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))
⊢ Eq (α := Subalgebra R R[M])
    (adjoin R (Set.image (α := M) (⇑(of R M) : (a : M) → R[M]) (⋃ f ∈ S, (↑f.support : Set M)))) ⊤
have rw : Eq (α := Subalgebra R R[M]) (adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) ⊤
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
⊢ Eq (α := Subalgebra R R[M])
    (adjoin R (Set.image (α := M) (⇑(of R M) : (a : M) → R[M]) (⋃ f ∈ S, (↑f.support : Set M)))) ⊤
have suffices : Eq (α := Set R[M]) (Set.image (α := M) (⇑(of R M) : (a : M) → R[M]) (⋃ f ∈ S, (↑f.support : Set M)))
  (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))
Tactic: suffices (of R M '' ⋃ f ∈ S, (f.support : Set M)) = ⋃ f ∈ S, of R M '' (f.support : Set M) by
    rw [this]
    exact support_gen_of_gen hS
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Monoid M
h : FiniteType R R[M]
⊢ ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑G : Set M))) ⊤
have obtain : ∀ (S : Finset R[M]) (hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤),
  ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑G : Set M))) ⊤
Tactic: obtain ⟨S, hS⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Monoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this : DecidableEq M := Classical.decEq M
⊢ ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑G : Set M))) ⊤
have h : Eq (α := Subalgebra R R[M])
  (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M))) ⊤
Tactic: use Finset.biUnion S fun f => f.support
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Monoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this : DecidableEq M := Classical.decEq M
⊢ Eq (α := Subalgebra R R[M])
    (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M))) ⊤
have this₁ : (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)
Tactic: have : (Finset.biUnion S fun f => f.support : Set M) = ⋃ f ∈ S, (f.support : Set M) := by
    simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Monoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this_1 : DecidableEq M := Classical.decEq M
this : (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)
⊢ Eq (α := Subalgebra R R[M])
    (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M))) ⊤
have h : Eq (α := Subalgebra R R[M]) (adjoin R (Set.image (α := M) (⇑(of R M) : (a : M) → R[M]) (⋃ f ∈ S, (↑f.support : Set M))))
  ⊤
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
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 : (a : M) → 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 : M) → R[M]) m : R[M])
have this : Membership.mem (γ := Submonoid M) (closure S) m
Tactic: have : m ∈ closure S := hS.symm ▸ mem_top _
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) 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 : (a : M) → 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 : M) → R[M]) m : R[M])
have 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 : (a : M) → 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 : M) → R[M]) m : R[M])
Tactic: refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid 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 : (a : M) → 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 : M) → R[M]) m : 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 : (a : M) → 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 : M) → R[M]) m : R[M])
have 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 : (a : M) → 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 : M) → R[M]) 1 : R[M])
Tactic: refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid 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 : (a : M) → 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 : M) → R[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 : (a : M) → 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 : M) → R[M]) 1 : 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 : (a : M) → 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 : M) → R[M]) m : R[M])
have hM₂ : ∀ (x y : M) (hx : Membership.mem (γ := Submonoid M) (closure S) x)
  (hy : Membership.mem (γ := Submonoid 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 : (a : M) → 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 : M) → R[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 : (a : M) → 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 : M) → R[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 : (a : M) → 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 : M) → R[M]) (x * y) : R[M])
Tactic: refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₁ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → 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])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R
hP₂ :
  Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → 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])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
⊢ Eq (α := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → 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])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])
have rw : HMul.hMul (α := R[M]) (β := R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → 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])
        P₁ :
      R[M])
    (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → 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])
        P₂ :
      R[M]) =
  (of R M : (a : M) → R[M]) (m₁ * m₂)
Tactic: rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]