case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a}
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a} = ⊤
apply top_unique
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ AddSubmonoid.closure
      (↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ''
        {f | ∃ a b, f = Finsupp.single a b}) ≤
    AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a}
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a}
rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ←
  Finsupp.add_closure_setOf_eq_single, AddMonoidHom.map_mclosure]
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ {f | ∃ a b, f = Finsupp.single a b} ⊆
    ↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ⁻¹'
      {p | ∃ n a, p = ↑(monomial n) a}
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ AddSubmonoid.closure
      (↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ''
        {f | ∃ a b, f = Finsupp.single a b}) ≤
    AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a}
refine' AddSubmonoid.closure_mono (Set.image_subset_iff.2 _)
case h.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ Finsupp.single n a ∈
    ↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ⁻¹'
      {p | ∃ n a, p = ↑(monomial n) a}
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ {f | ∃ a b, f = Finsupp.single a b} ⊆
    ↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ⁻¹'
      {p | ∃ n a, p = ↑(monomial n) a}
rintro _ ⟨n, a, rfl⟩
no goals
case h.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ Finsupp.single n a ∈
    ↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ⁻¹'
      {p | ∃ n a, p = ↑(monomial n) a}
exact ⟨n, a, Polynomial.ofFinsupp_single _ _⟩