R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : MonoidAlgebra R M
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
⊢ Surjective ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s)
intro f
case hM
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) m

case hadd
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : MonoidAlgebra R M
ihf : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f
ihg : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = g
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f + g

case hsmul
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : MonoidAlgebra R M
ih : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = r • f
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : MonoidAlgebra R M
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f
induction' f using induction_on with m f g ihf ihg r f ih
case hM
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) m
case hM
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) m
have : m ∈ closure S := hS.symm ▸ mem_top _
case hM.refine'_1
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) m

case hM.refine'_2
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) 1

case hM.refine'_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    (∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) x) →
      (∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) y) →
        ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) (x * y)
case hM
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) m
refine' closure_induction this (fun m hm => _) _ _
no goals
case hM.refine'_1
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) m
exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
no goals
case hM.refine'_2
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) 1
exact ⟨1, AlgHom.map_one _⟩
case hM.refine'_3.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
P₁ : MvPolynomial (↑S) R
hP₁ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₁ = ↑(of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₂ = ↑(of R M) m₂
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) (m₁ * m₂)
case hM.refine'_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    (∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) x) →
      (∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) y) →
        ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) (x * y)
rintro m₁ m₂ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
no goals
case hM.refine'_3.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
P₁ : MvPolynomial (↑S) R
hP₁ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₁ = ↑(of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₂ = ↑(of R M) m₂
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) (m₁ * m₂)
exact
  ⟨P₁ * P₂, by
    rw [AlgHom.map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩
no goals
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
P₁ : MvPolynomial (↑S) R
hP₁ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₁ = ↑(of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₂ = ↑(of R M) m₂
⊢ ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) (P₁ * P₂) = ↑(of R M) (m₁ * m₂)
rw [AlgHom.map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : MonoidAlgebra R M
ihg : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = g
P : MvPolynomial (↑S) R
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P + g
case hadd
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : MonoidAlgebra R M
ihf : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f
ihg : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = g
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f + g
rcases ihf with ⟨P, rfl⟩
case hadd.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : MvPolynomial (↑S) R
⊢ ∃ a,
    ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a =
      ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P + ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) Q
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : MonoidAlgebra R M
ihg : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = g
P : MvPolynomial (↑S) R
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P + g
rcases ihg with ⟨Q, rfl⟩
no goals
case hadd.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : MvPolynomial (↑S) R
⊢ ∃ a,
    ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a =
      ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P + ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) Q
exact ⟨P + Q, AlgHom.map_add _ _ _⟩
case hsmul.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : MvPolynomial (↑S) R
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = r • ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P
case hsmul
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : MonoidAlgebra R M
ih : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = r • f
rcases ih with ⟨P, rfl⟩
no goals
case hsmul.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : MvPolynomial (↑S) R
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = r • ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P
exact ⟨r • P, AlgHom.map_smul _ _ _⟩