R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) =
    ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ adjoin R (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
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
no goals
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) =
    ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support
simp only [Set.image_iUnion]
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
this :
  (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) =
    ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support
⊢ adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support) = ⊤
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
this :
  (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) =
    ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support
⊢ adjoin R (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
rw [this]
no goals
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
this :
  (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) =
    ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support
⊢ adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support) = ⊤
exact support_gen_of_gen hS