case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
⊢ ∃ G, adjoin R (↑(of R M) '' ↑G) = ⊤
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
h : FiniteType R (MonoidAlgebra R M)
⊢ ∃ G, adjoin R (↑(of R M) '' ↑G) = ⊤
obtain ⟨S, hS⟩ := h
case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ∃ G, adjoin R (↑(of R M) '' ↑G) = ⊤
case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
⊢ ∃ G, adjoin R (↑(of R M) '' ↑G) = ⊤
letI : DecidableEq M := Classical.decEq M
case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ adjoin R (↑(of R M) '' ↑(Finset.biUnion S fun f => f.support)) = ⊤
case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ∃ G, adjoin R (↑(of R M) '' ↑G) = ⊤
use Finset.biUnion S fun f => f.support
case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support
⊢ adjoin R (↑(of R M) '' ↑(Finset.biUnion S fun f => f.support)) = ⊤
case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ adjoin R (↑(of R M) '' ↑(Finset.biUnion S fun f => f.support)) = ⊤
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]
case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support
⊢ adjoin R (↑(of R M) '' ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support
⊢ adjoin R (↑(of R M) '' ↑(Finset.biUnion S fun f => f.support)) = ⊤
rw [this]
no goals
case mk.intro
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support
⊢ adjoin R (↑(of R M) '' ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
exact support_gen_of_gen' hS
no goals
R : Type u_2
M : Type u_1
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support
simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]