-- Mathlib/RingTheory/FiniteType.lean
theorem exists_finset_adjoin_eq_top [h : FiniteType R R[M]] :
    ∃ G : Finset M, Algebra.adjoin R (of' R M '' G) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
h : FiniteType R R[M]
⊢ ∃ G, adjoin R (of' R M '' ↑G) = ⊤

Tactic:
obtain ⟨S, hS⟩ := h

Result:
case mk.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
⊢ ∃ G, adjoin R (of' R M '' ↑G) = ⊤

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ adjoin R (of' R M '' ↑(S.biUnion fun f => f.support)) = ⊤

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]

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f => f.support) = ⋃ f ∈ S, ↑f.support
⊢ adjoin R (of' R M '' ↑(S.biUnion fun f => f.support)) = ⊤

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f => f.support) = ⋃ f ∈ S, ↑f.support
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.support) = ⊤

Tactic:
exact support_gen_of_gen' hS

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f => f.support) = ⋃ f ∈ S, ↑f.support
⊢ adjoin R (of' R M '' ↑(S.biUnion fun f => f.support)) = ⊤

Tactic:
rw [this]

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f => f.support) = ⋃ f ∈ S, ↑f.support
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.support) = ⊤

Proof state:
case mk.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ∃ G, adjoin R (of' R M '' ↑G) = ⊤

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

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ adjoin R (of' R M '' ↑(S.biUnion fun f => f.support)) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ↑(S.biUnion fun f => f.support) = ⋃ f ∈ S, ↑f.support

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

Result:
no goals

Proof state:
case mk.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
⊢ ∃ G, adjoin R (of' R M '' ↑G) = ⊤

Tactic:
letI : DecidableEq M := Classical.decEq M

Result:
case mk.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ∃ G, adjoin R (of' R M '' ↑G) = ⊤