[GOAL]
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
⊢ x ∈ Ideal.span (↑(of k G) '' s) ↔ ∀ (m : G), m ∈ x.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
let RHS : Ideal (MonoidAlgebra k G) :=
  { carrier := {p | ∀ m : G, m ∈ p.support → ∃ m' ∈ s, ∃ d, m = d * m'}
    add_mem' := fun {x y} hx hy m hm => by
      classical exact (Finset.mem_union.1 <| Finsupp.support_add hm).elim (hx m) (hy m)
    zero_mem' := fun m hm => by cases hm
    smul_mem' := fun x y hy m hm => by
      classical
      replace hm := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
      obtain ⟨xm, -, hm⟩ := hm
      replace hm := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
      obtain ⟨ym, hym, hm⟩ := hm
      replace hm := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
      obtain rfl := hm
      refine' (hy _ hym).imp fun sm p => And.imp_right _ p
      rintro ⟨d, rfl⟩
      exact ⟨xm * d, (mul_assoc _ _ _).symm⟩ }
[GOAL]
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hx : x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'}
hy : y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'}
m : G
hm : m ∈ (x + y).support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
classical exact (Finset.mem_union.1 <| Finsupp.support_add hm).elim (hx m) (hy m)
[GOAL]
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hx : x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'}
hy : y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'}
m : G
hm : m ∈ (x + y).support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
exact (Finset.mem_union.1 <| Finsupp.support_add hm).elim (hx m) (hy m)
[GOAL]
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
m : G
hm : m ∈ 0.support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
cases hm
[GOAL]
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
m : G
hm : m ∈ (x • y).support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
classical
replace hm := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
obtain ⟨xm, -, hm⟩ := hm
replace hm := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
obtain ⟨ym, hym, hm⟩ := hm
replace hm := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
obtain rfl := hm
refine' (hy _ hym).imp fun sm p => And.imp_right _ p
rintro ⟨d, rfl⟩
exact ⟨xm * d, (mul_assoc _ _ _).symm⟩
[GOAL]
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
m : G
hm : m ∈ (x • y).support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
replace hm := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
[GOAL]
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
m : G
hm : ∃ a, a ∈ x.support ∧ m ∈ (Finsupp.sum y fun a₂ b₂ => single (a * a₂) (↑x a * b₂)).support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
obtain ⟨xm, -, hm⟩ := hm
[GOAL]
case intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
m xm : G
hm : m ∈ (Finsupp.sum y fun a₂ b₂ => single (xm * a₂) (↑x xm * b₂)).support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
replace hm := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
[GOAL]
case intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
m xm : G
hm : ∃ a, a ∈ y.support ∧ m ∈ (single (xm * a) (↑x xm * ↑y a)).support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
obtain ⟨ym, hym, hm⟩ := hm
[GOAL]
case intro.intro.intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
m xm ym : G
hym : ym ∈ y.support
hm : m ∈ (single (xm * ym) (↑x xm * ↑y ym)).support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
replace hm := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
[GOAL]
case intro.intro.intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
m xm ym : G
hym : ym ∈ y.support
hm : m = xm * ym
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
obtain rfl := hm
[GOAL]
case intro.intro.intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
xm ym : G
hym : ym ∈ y.support
⊢ ∃ m', m' ∈ s ∧ ∃ d, xm * ym = d * m'
[PROOFSTEP]
refine' (hy _ hym).imp fun sm p => And.imp_right _ p
[GOAL]
case intro.intro.intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
xm ym : G
hym : ym ∈ y.support
sm : G
p : sm ∈ s ∧ ∃ d, ym = d * sm
⊢ (∃ d, ym = d * sm) → ∃ d, xm * ym = d * sm
[PROOFSTEP]
rintro ⟨d, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : MonoidAlgebra k G
hy :
  y ∈
    {
          toAddSubsemigroup :=
            { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
              add_mem' :=
                (_ :
                  ∀ {x y : MonoidAlgebra k G},
                    x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                        ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
          zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier
xm sm d : G
hym : d * sm ∈ y.support
p : sm ∈ s ∧ ∃ d_1, d * sm = d_1 * sm
⊢ ∃ d_1, xm * (d * sm) = d_1 * sm
[PROOFSTEP]
exact ⟨xm * d, (mul_assoc _ _ _).symm⟩
[GOAL]
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
⊢ x ∈ Ideal.span (↑(of k G) '' s) ↔ ∀ (m : G), m ∈ x.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
change _ ↔ x ∈ RHS
[GOAL]
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
⊢ x ∈ Ideal.span (↑(of k G) '' s) ↔ x ∈ RHS
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
⊢ x ∈ Ideal.span (↑(of k G) '' s) → x ∈ RHS
[PROOFSTEP]
revert x
[GOAL]
case mp
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
⊢ ∀ {x : MonoidAlgebra k G}, x ∈ Ideal.span (↑(of k G) '' s) → x ∈ RHS
[PROOFSTEP]
rw [← SetLike.le_def]
  -- porting note: refine needs this even though it's defeq?
[GOAL]
case mp
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
⊢ Ideal.span (↑(of k G) '' s) ≤ RHS
[PROOFSTEP]
refine Ideal.span_le.2 ?_
[GOAL]
case mp
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
⊢ ↑(of k G) '' s ⊆ ↑RHS
[PROOFSTEP]
rintro _ ⟨i, hi, rfl⟩ m hm
[GOAL]
case mp.intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
i : G
hi : i ∈ s
m : G
hm : m ∈ (↑(of k G) i).support
⊢ ∃ m', m' ∈ s ∧ ∃ d, m = d * m'
[PROOFSTEP]
refine' ⟨_, hi, 1, _⟩
[GOAL]
case mp.intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
i : G
hi : i ∈ s
m : G
hm : m ∈ (↑(of k G) i).support
⊢ m = 1 * i
[PROOFSTEP]
obtain rfl := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
[GOAL]
case mp.intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
m : G
hi : m ∈ s
hm : m ∈ (↑(of k G) m).support
⊢ m = 1 * m
[PROOFSTEP]
exact (one_mul _).symm
[GOAL]
case mpr
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
⊢ x ∈ RHS → x ∈ Ideal.span (↑(of k G) '' s)
[PROOFSTEP]
intro hx
[GOAL]
case mpr
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
⊢ x ∈ Ideal.span (↑(of k G) '' s)
[PROOFSTEP]
rw [← Finsupp.sum_single x]
[GOAL]
case mpr
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
⊢ Finsupp.sum x Finsupp.single ∈ Ideal.span (↑(of k G) '' s)
[PROOFSTEP]
refine
  Ideal.sum_mem _ fun i hi =>
    ?_
      -- porting note: changed `apply` to `refine`
[GOAL]
case mpr
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
i : G
hi : i ∈ x.support
⊢ Finsupp.single i (↑x i) ∈ Ideal.span (↑(of k G) '' s)
[PROOFSTEP]
obtain ⟨d, hd, d2, rfl⟩ := hx _ hi
[GOAL]
case mpr.intro.intro.intro
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.support
⊢ Finsupp.single (d2 * d) (↑x (d2 * d)) ∈ Ideal.span (↑(of k G) '' s)
[PROOFSTEP]
convert Ideal.mul_mem_left _ (id <| Finsupp.single d2 <| x (d2 * d) : MonoidAlgebra k G) _
[GOAL]
case h.e'_4
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.support
⊢ Finsupp.single (d2 * d) (↑x (d2 * d)) = id (Finsupp.single d2 (↑x (d2 * d))) * ?mpr.intro.intro.intro.convert_2
case mpr.intro.intro.intro.convert_2
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.support
⊢ MonoidAlgebra k G
case mpr.intro.intro.intro.convert_3
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.support
⊢ ?mpr.intro.intro.intro.convert_2 ∈ Ideal.span (↑(of k G) '' s)
[PROOFSTEP]
pick_goal 3
[GOAL]
case mpr.intro.intro.intro.convert_3
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.support
⊢ ?mpr.intro.intro.intro.convert_2 ∈ Ideal.span (↑(of k G) '' s)
case h.e'_4
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.support
⊢ Finsupp.single (d2 * d) (↑x (d2 * d)) = id (Finsupp.single d2 (↑x (d2 * d))) * ?mpr.intro.intro.intro.convert_2
case mpr.intro.intro.intro.convert_2
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.support
⊢ MonoidAlgebra k G
[PROOFSTEP]
refine' Ideal.subset_span ⟨_, hd, rfl⟩
[GOAL]
case h.e'_4
k : Type u_1
A : Type u_2
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : MonoidAlgebra k G
RHS : Ideal (MonoidAlgebra k G) :=
  {
    toAddSubmonoid :=
      {
        toAddSubsemigroup :=
          { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
            add_mem' :=
              (_ :
                ∀ {x y : MonoidAlgebra k G},
                  x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                    y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                      ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
        zero_mem' := (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
    smul_mem' :=
      (_ :
        ∀ (x y : MonoidAlgebra k G),
          y ∈
              {
                    toAddSubsemigroup :=
                      { carrier := {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'},
                        add_mem' :=
                          (_ :
                            ∀ {x y : MonoidAlgebra k G},
                              x ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                y ∈ {p | ∀ (m : G), m ∈ p.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m'} →
                                  ∀ (m : G), m ∈ (x + y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') },
                    zero_mem' :=
                      (_ : ∀ (m : G), m ∈ 0.support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }.toAddSubsemigroup.carrier →
            ∀ (m : G), m ∈ (x • y).support → ∃ m', m' ∈ s ∧ ∃ d, m = d * m') }
hx : x ∈ RHS
d : G
hd : d ∈ s
d2 : G
hi : d2 * d ∈ x.support
⊢ Finsupp.single (d2 * d) (↑x (d2 * d)) = id (Finsupp.single d2 (↑x (d2 * d))) * ↑(of k G) d
[PROOFSTEP]
rw [id.def, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
