R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ ⊤ ≤ adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support)
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ adjoin R (⋃ (f : MonoidAlgebra 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✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support))
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ ⊤ ≤ adjoin R (⋃ (f : MonoidAlgebra 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✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support))
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support))
intro f hf
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
hincl : ↑(of R M) '' ↑f.support ⊆ ⋃ (g : MonoidAlgebra R M) (_ : g ∈ S), ↑(of R M) '' ↑g.support
⊢ f ∈ ↑(adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support))
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support))
have hincl : (of R M '' f.support) ⊆
    Set.iUnion fun (g : MonoidAlgebra R M)
      => Set.iUnion fun (_ : 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✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
hincl : ↑(of R M) '' ↑f.support ⊆ ⋃ (g : MonoidAlgebra R M) (_ : g ∈ S), ↑(of R M) '' ↑g.support
⊢ f ∈ ↑(adjoin R (⋃ (f : MonoidAlgebra 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✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
s : MonoidAlgebra R M
hs : s ∈ ↑(of R M) '' ↑f.support
⊢ s ∈ ⋃ (g : MonoidAlgebra R M) (_ : g ∈ S), ↑(of R M) '' ↑g.support
R : Type u_2
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
⊢ ↑(of R M) '' ↑f.support ⊆ ⋃ (g : MonoidAlgebra 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✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
s : MonoidAlgebra R M
hs : s ∈ ↑(of R M) '' ↑f.support
⊢ s ∈ ⋃ (g : MonoidAlgebra R M) (_ : g ∈ S), ↑(of R M) '' ↑g.support
exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩