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 (⋃ (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 (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support) = ⊤
refine' le_antisymm le_top _
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(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 = ⊤
⊢ ⊤ ≤ adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support)
rw [← hS, adjoin_le_iff]
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
⊢ f ∈ ↑(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 = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support))
intro f hf
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
hincl : of' R M '' ↑f.support ⊆ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' ↑g.support
⊢ f ∈ ↑(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 = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support))
have hincl :
  of' R M '' f.support ⊆ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' g.support := by
  intro s hs
  exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, 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 = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
hincl : of' R M '' ↑f.support ⊆ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' ↑g.support
⊢ f ∈ ↑(adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support))
exact adjoin_mono hincl (mem_adjoin_support f)
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
s : AddMonoidAlgebra R M
hs : s ∈ of' R M '' ↑f.support
⊢ s ∈ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' ↑g.support
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
⊢ of' R M '' ↑f.support ⊆ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' ↑g.support
intro s 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 = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
s : AddMonoidAlgebra R M
hs : s ∈ of' R M '' ↑f.support
⊢ s ∈ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' ↑g.support
exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩