awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteType
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) ⊤
P Q : 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 =
      HAdd.hAdd (α := R[M]) (β := 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])
            P :
          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])
            Q :
          R[M])

Tactic:
exact ⟨P + Q, map_add _ _ _⟩
-- Module: Mathlib.RingTheory.FiniteType
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
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])
⊢ ∃ (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

Tactic:
rcases ih with ⟨P, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FiniteType
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
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:
⟨r • P, map_smul _ _ _⟩

Premises used: Exists.intro, HSMul.hSMul, map_smul
-- Module: Mathlib.RingTheory.FiniteType
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
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:
exact ⟨r • P, map_smul _ _ _⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
h : AddMonoid.FG M
obtain : ∀ (S : Finset M) (hS : Eq (α := AddSubmonoid M) (closure (↑S : Set M)) ⊤), FiniteType R R[M]
⊢ FiniteType R R[M]

Tactic:
obtain ⟨S, hS⟩ := h.fg_top

Premises used: AddMonoid.FG.fg_top
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
h : AddMonoid.FG M
S : Finset M
hS : Eq (α := AddSubmonoid M) (closure (↑S : Set M)) ⊤
⊢ FiniteType R R[M]

Tactic:
.of_surjective
      (FreeAlgebra.lift R fun s : (S : Set M) => of' R M ↑s)
      (freeAlgebra_lift_of_surjective_of_closure hS)

Premises used: Algebra.FiniteType.of_surjective, FreeAlgebra.lift, AddMonoidAlgebra.of', Subtype.val, DFunLike.coe, AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
h : AddMonoid.FG M
S : Finset M
hS : Eq (α := AddSubmonoid M) (closure (↑S : Set M)) ⊤
⊢ FiniteType R R[M]

Tactic:
exact .of_surjective
      (FreeAlgebra.lift R fun s : (S : Set M) => of' R M ↑s)
      (freeAlgebra_lift_of_surjective_of_closure hS)
-- Module: Mathlib.RingTheory.FiniteType
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

Tactic:
⟨fun h => ?_, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩

Premises used: AddMonoidAlgebra.finiteType_of_fg, Iff.intro
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoid M
inst_1 : CommRing R
inst_2 : Nontrivial R
refine : ∀ (h : FiniteType R R[M]), AddMonoid.FG M
⊢ FiniteType R R[M] ↔ AddMonoid.FG M

Tactic:
refine ⟨fun h => ?_, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩
-- Module: Mathlib.RingTheory.FiniteType
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]
obtain : ∀ (S : Finset M) (hS : Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑S : Set M))) ⊤), AddMonoid.FG M
⊢ AddMonoid.FG M

Tactic:
obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h

Premises used: AddMonoidAlgebra.exists_finset_adjoin_eq_top
-- Module: Mathlib.RingTheory.FiniteType
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

Tactic:
AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => ?_⟩

Premises used: Iff.mpr, AddMonoid.fg_def, Exists.intro, AddSubmonoid.eq_top_iff'
-- Module: Mathlib.RingTheory.FiniteType
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))) ⊤
refine : ∀ (m : M), Membership.mem (γ := AddSubmonoid M) (closure (↑S : Set M)) m
⊢ AddMonoid.FG M

Tactic:
refine AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => ?_⟩

Premises used: Iff.mpr, AddMonoid.fg_def, Exists.intro, AddSubmonoid.eq_top_iff'
-- Module: Mathlib.RingTheory.FiniteType
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 (γ := 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:
simp only [hS, top_toSubmodule, Submodule.mem_top]

Premises used: Algebra.top_toSubmodule, Submodule.mem_top
-- Module: Mathlib.RingTheory.FiniteType
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 (γ := 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]
-- Module: Mathlib.RingTheory.FiniteType
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 (γ := 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

Premises used: Algebra.adjoin_eq_span
-- Module: Mathlib.RingTheory.FiniteType
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]) (span R (↑(Submonoid.closure (of' R M '' (↑S : Set M))) : Set R[M]))
    (of' R M m)
⊢ Membership.mem (γ := AddSubmonoid M) (closure (↑S : Set M)) m

Tactic:
mem_closure_of_mem_span_closure hm

Premises used: AddMonoidAlgebra.mem_closure_of_mem_span_closure
-- Module: Mathlib.RingTheory.FiniteType
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]) (span R (↑(Submonoid.closure (of' R M '' (↑S : Set M))) : Set R[M]))
    (of' R M m)
⊢ Membership.mem (γ := AddSubmonoid M) (closure (↑S : Set M)) m

Tactic:
exact mem_closure_of_mem_span_closure hm

Premises used: AddMonoidAlgebra.mem_closure_of_mem_span_closure
-- Module: Mathlib.RingTheory.FiniteType
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

Tactic:
finiteType_iff_fg.1 h

Premises used: Iff.mp, AddMonoidAlgebra.finiteType_iff_fg
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
G : Type u_3
inst : AddGroup G
inst_1 : CommRing R
inst_2 : Nontrivial R
⊢ FiniteType R R[G] ↔ AddGroup.FG G

Tactic:
simpa [AddGroup.fg_iff_addMonoid_fg] using finiteType_iff_fg

Premises used: AddGroup.fg_iff_addMonoid_fg, AddMonoidAlgebra.finiteType_iff_fg
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
f : R[M]
this :
  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))))
⊢ Membership.mem (γ := Subalgebra R R[M]) (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) f

Tactic:
this (mem_span_support f)

Premises used: iInf, Set.Mem, Set.iInter, setOf, MonoidAlgebra.mem_span_support
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
f : R[M]
this :
  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))))
⊢ Membership.mem (γ := Subalgebra R R[M]) (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) f

Tactic:
exact this (mem_span_support f)

Premises used: MonoidAlgebra.mem_span_support
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
f : R[M]
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))))
⊢ Membership.mem (γ := Subalgebra R R[M]) (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) f

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)
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
f : R[M]
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])
⊢ 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:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
f : R[M]
⊢ (⇑(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:
subset_adjoin

Premises used: iInf, Set.iInter, Algebra.subset_adjoin, setOf
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Monoid M
f : R[M]
⊢ (⇑(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:
exact subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.FiniteType
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))) ⊤

Tactic:
le_antisymm le_top ?_

Premises used: le_antisymm, le_top
-- Module: Mathlib.RingTheory.FiniteType
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) ⊤
refine : LE.le (α := Subalgebra R R[M]) ⊤ (adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M)))
⊢ Eq (α := 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 ?_

Premises used: le_antisymm, le_top
-- Module: Mathlib.RingTheory.FiniteType
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) ⊤
rw : S ⊆ (↑(adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) : Set R[M])
⊢ LE.le (α := Subalgebra R R[M]) ⊤ (adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M)))

Tactic:
rw [← hS, adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff
-- Module: Mathlib.RingTheory.FiniteType
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
s : R[M]
hs : Membership.mem (γ := Set R[M]) ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M)) s
⊢ Membership.mem (γ := Set R[M]) (⋃ g ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑g.support : Set M)) s

Tactic:
Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.RingTheory.FiniteType
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
s : R[M]
hs : Membership.mem (γ := Set R[M]) ((⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M)) s
⊢ Membership.mem (γ := Set R[M]) (⋃ g ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑g.support : Set M)) s

Tactic:
exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.RingTheory.FiniteType
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
⊢ 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⟩⟩
-- Module: Mathlib.RingTheory.FiniteType
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
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))
⊢ f ∈ (↑(adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) : Set R[M])

Tactic:
adjoin_mono hincl (mem_adjoin_support f)

Premises used: MonoidAlgebra.mem_adjoin_support, Set.Mem, setOf, Algebra.adjoin_mono
-- Module: Mathlib.RingTheory.FiniteType
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
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))
⊢ f ∈ (↑(adjoin R (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) : Set R[M])

Tactic:
exact adjoin_mono hincl (mem_adjoin_support f)

Premises used: MonoidAlgebra.mem_adjoin_support, Algebra.adjoin_mono
-- Module: Mathlib.RingTheory.FiniteType
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))
rw : Eq (α := Subalgebra R R[M]) (adjoin R (⋃ 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)))) ⊤

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.FiniteType
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 (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) ⊤

Tactic:
support_gen_of_gen hS

Premises used: MonoidAlgebra.support_gen_of_gen
-- Module: Mathlib.RingTheory.FiniteType
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 (⋃ f ∈ S, (⇑(of R M) : (a : M) → R[M]) '' (↑f.support : Set M))) ⊤

Tactic:
exact support_gen_of_gen hS

Premises used: MonoidAlgebra.support_gen_of_gen
-- Module: Mathlib.RingTheory.FiniteType
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) ⊤
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))
⊢ Eq (α := Subalgebra R R[M])
    (adjoin R (Set.image (α := M) (⇑(of R M) : (a : M) → R[M]) (⋃ f ∈ S, (↑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
-- Module: Mathlib.RingTheory.FiniteType
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 (α := 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:
simp only [Set.image_iUnion]

Premises used: Set.image_iUnion
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Monoid M
h : FiniteType R R[M]
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))) ⊤
⊢ ∃ (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
-- Module: Mathlib.RingTheory.FiniteType
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
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))) ⊤
⊢ ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R ((⇑(of R M) : (a : M) → R[M]) '' (↑G : Set M))) ⊤

Tactic:
use Finset.biUnion S fun f => f.support

Premises used: Finsupp.support, Finset.biUnion
-- Module: Mathlib.RingTheory.FiniteType
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
⊢ (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)

Tactic:
simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]

Premises used: Finset.coe_biUnion, Finset.set_biUnion_coe
-- Module: Mathlib.RingTheory.FiniteType
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
⊢ (↑(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]
-- Module: Mathlib.RingTheory.FiniteType
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)
h :
  Eq (α := Subalgebra R R[M])
    (adjoin R (Set.image (α := M) (⇑(of R M) : (a : M) → R[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))) ⊤

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.FiniteType
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 (Set.image (α := M) (⇑(of R M) : (a : M) → R[M]) (⋃ f ∈ S, (↑f.support : Set M)))) ⊤

Tactic:
support_gen_of_gen' hS

Premises used: MonoidAlgebra.support_gen_of_gen'