[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]


[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a : G
⊢ (single a r * f).support ⊆ image ((fun x x_1 => x * x_1) a) f.support
[PROOFSTEP]
intro x hx
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : x ∈ (single a r * f).support
⊢ x ∈ image ((fun x x_1 => x * x_1) a) f.support
[PROOFSTEP]
contrapose hx
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image ((fun x x_1 => x * x_1) a) f.support
⊢ ¬x ∈ (single a r * f).support
[PROOFSTEP]
have : ∀ y, a * y = x → f y = 0 := by
  simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, Classical.not_not] using hx
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image ((fun x x_1 => x * x_1) a) f.support
⊢ ∀ (y : G), a * y = x → ↑f y = 0
[PROOFSTEP]
simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, Classical.not_not] using hx
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image ((fun x x_1 => x * x_1) a) f.support
this : ∀ (y : G), a * y = x → ↑f y = 0
⊢ ¬x ∈ (single a r * f).support
[PROOFSTEP]
simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, ite_self, sum_zero, Classical.not_not]
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image ((fun x x_1 => x * x_1) a) f.support
this : ∀ (y : G), a * y = x → ↑f y = 0
⊢ (sum f fun a₂ b₂ => if a * a₂ = x then r * b₂ else 0) = 0
[PROOFSTEP]
exact
  Finset.sum_eq_zero
    (by
      simp (config := { contextual := true }) only [this, mem_support_iff, mul_zero, Ne.def, ite_eq_right_iff,
        eq_self_iff_true, imp_true_iff])
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image ((fun x x_1 => x * x_1) a) f.support
this : ∀ (y : G), a * y = x → ↑f y = 0
⊢ ∀ (x_1 : G), x_1 ∈ f.support → (fun a₂ b₂ => if a * a₂ = x then r * b₂ else 0) x_1 (↑f x_1) = 0
[PROOFSTEP]
simp (config := { contextual := true }) only [this, mem_support_iff, mul_zero, Ne.def, ite_eq_right_iff,
  eq_self_iff_true, imp_true_iff]
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a : G
⊢ (f * single a r).support ⊆ image (fun x => x * a) f.support
[PROOFSTEP]
intro x hx
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : x ∈ (f * single a r).support
⊢ x ∈ image (fun x => x * a) f.support
[PROOFSTEP]
contrapose hx
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
⊢ ¬x ∈ (f * single a r).support
[PROOFSTEP]
have : ∀ y, y * a = x → f y = 0 := by
  simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, Classical.not_not] using hx
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
⊢ ∀ (y : G), y * a = x → ↑f y = 0
[PROOFSTEP]
simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, Classical.not_not] using hx
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
this : ∀ (y : G), y * a = x → ↑f y = 0
⊢ ¬x ∈ (f * single a r).support
[PROOFSTEP]
simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, ite_self, sum_zero, Classical.not_not]
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
this : ∀ (y : G), y * a = x → ↑f y = 0
⊢ (sum f fun a₁ b₁ => sum (single a r) fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0) = 0
[PROOFSTEP]
exact
  Finset.sum_eq_zero
    (by
      simp (config := { contextual := true }) only [this, sum_single_index, ite_eq_right_iff, eq_self_iff_true,
        imp_true_iff, zero_mul])
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a x : G
hx : ¬x ∈ image (fun x => x * a) f.support
this : ∀ (y : G), y * a = x → ↑f y = 0
⊢ ∀ (x_1 : G),
    x_1 ∈ f.support → (fun a₁ b₁ => sum (single a r) fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0) x_1 (↑f x_1) = 0
[PROOFSTEP]
simp (config := { contextual := true }) only [this, sum_single_index, ite_eq_right_iff, eq_self_iff_true, imp_true_iff,
  zero_mul]
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
⊢ (single x r * f).support = image ((fun x x_1 => x * x_1) x) f.support
[PROOFSTEP]
refine' subset_antisymm (support_single_mul_subset f _ _) fun y hy => _
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : y ∈ image ((fun x x_1 => x * x_1) x) f.support
⊢ y ∈ (single x r * f).support
[PROOFSTEP]
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by simpa only [Finset.mem_image, exists_prop] using hy
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : y ∈ image ((fun x x_1 => x * x_1) x) f.support
⊢ ∃ a, a ∈ f.support ∧ x * a = y
[PROOFSTEP]
simpa only [Finset.mem_image, exists_prop] using hy
[GOAL]
case intro.intro
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
yf : y ∈ f.support
hy : x * y ∈ image ((fun x x_1 => x * x_1) x) f.support
⊢ x * y ∈ (single x r * f).support
[PROOFSTEP]
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index, Finsupp.sum_ite_eq', Ne.def,
  not_false_iff, if_true, zero_mul, ite_self, sum_zero, lx.eq_iff]
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
⊢ (f * single x r).support = image (fun x_1 => x_1 * x) f.support
[PROOFSTEP]
refine' subset_antisymm (support_mul_single_subset f _ _) fun y hy => _
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 => x_1 * x) f.support
⊢ y ∈ (f * single x r).support
[PROOFSTEP]
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ a * x = y := by simpa only [Finset.mem_image, exists_prop] using hy
[GOAL]
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 => x_1 * x) f.support
⊢ ∃ a, a ∈ f.support ∧ a * x = y
[PROOFSTEP]
simpa only [Finset.mem_image, exists_prop] using hy
[GOAL]
case intro.intro
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
yf : y ∈ f.support
hy : y * x ∈ image (fun x_1 => x_1 * x) f.support
⊢ y * x ∈ (f * single x r).support
[PROOFSTEP]
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index, Finsupp.sum_ite_eq', Ne.def,
  not_false_iff, if_true, mul_zero, ite_self, sum_zero, rx.eq_iff]
[GOAL]
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : RightCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support
[PROOFSTEP]
classical
ext
simp only [support_mul_single_eq_image f hr (isRightRegular_of_rightCancelSemigroup x), mem_image, mem_map,
  mulRightEmbedding_apply]
[GOAL]
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : RightCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support
[PROOFSTEP]
ext
[GOAL]
case a
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : RightCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (f * single x r).support ↔ a✝ ∈ map (mulRightEmbedding x) f.support
[PROOFSTEP]
simp only [support_mul_single_eq_image f hr (isRightRegular_of_rightCancelSemigroup x), mem_image, mem_map,
  mulRightEmbedding_apply]
[GOAL]
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : LeftCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support
[PROOFSTEP]
classical
ext
simp only [support_single_mul_eq_image f hr (isLeftRegular_of_leftCancelSemigroup x), mem_image, mem_map,
  mulLeftEmbedding_apply]
[GOAL]
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : LeftCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support
[PROOFSTEP]
ext
[GOAL]
case a
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : LeftCancelSemigroup G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (single x r * f).support ↔ a✝ ∈ map (mulLeftEmbedding x) f.support
[PROOFSTEP]
simp only [support_single_mul_eq_image f hr (isLeftRegular_of_leftCancelSemigroup x), mem_image, mem_map,
  mulLeftEmbedding_apply]
[GOAL]
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : MulOneClass G
f : MonoidAlgebra k G
⊢ f ∈ Submodule.span k (↑(of k G) '' ↑f.support)
[PROOFSTEP]
erw [of, MonoidHom.coe_mk, ← supported_eq_span_single, Finsupp.mem_supported]
[GOAL]
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddZeroClass G
f : AddMonoidAlgebra k G
⊢ f ∈ Submodule.span k (↑(of k G) '' ↑f.support)
[PROOFSTEP]
erw [of, MonoidHom.coe_mk, ← Finsupp.supported_eq_span_single, Finsupp.mem_supported]
[GOAL]
k : Type u₁
G : Type u₂
inst✝ : Semiring k
f : AddMonoidAlgebra k G
⊢ f ∈ Submodule.span k (of' k G '' ↑f.support)
[PROOFSTEP]
delta of'
[GOAL]
k : Type u₁
G : Type u₂
inst✝ : Semiring k
f : AddMonoidAlgebra k G
⊢ f ∈ Submodule.span k ((fun a => single a 1) '' ↑f.support)
[PROOFSTEP]
rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]


[GOAL]
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n : ℕ
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
induction' m with m ih generalizing n
[GOAL]
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n✝ : ℕ
h✝ : ↑m = ↑n✝
n : ℕ
h : ↑Nat.zero = ↑n
⊢ Nat.zero = n
[PROOFSTEP]
rw [H n]
[GOAL]
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n✝ : ℕ
h✝ : ↑m = ↑n✝
n : ℕ
h : ↑Nat.zero = ↑n
⊢ ↑n = 0
[PROOFSTEP]
rw [← h, Nat.cast_zero]
[GOAL]
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n✝ : ℕ
h✝ : ↑m✝ = ↑n✝
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n : ℕ
h : ↑(Nat.succ m) = ↑n
⊢ Nat.succ m = n
[PROOFSTEP]
cases' n with n
[GOAL]
case succ.zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n : ℕ
h✝ : ↑m✝ = ↑n
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(Nat.succ m) = ↑Nat.zero
⊢ Nat.succ m = Nat.zero
[PROOFSTEP]
apply H
[GOAL]
case succ.zero.a
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n : ℕ
h✝ : ↑m✝ = ↑n
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(Nat.succ m) = ↑Nat.zero
⊢ ↑(Nat.succ m) = 0
[PROOFSTEP]
rw [h, Nat.cast_zero]
[GOAL]
case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n✝ : ℕ
h✝ : ↑m✝ = ↑n✝
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n : ℕ
h : ↑(Nat.succ m) = ↑(Nat.succ n)
⊢ Nat.succ m = Nat.succ n
[PROOFSTEP]
simp only [Nat.cast_succ, add_right_cancel_iff] at h
[GOAL]
case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m✝ n✝ : ℕ
h✝ : ↑m✝ = ↑n✝
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n : ℕ
h : ↑m = ↑n
⊢ Nat.succ m = Nat.succ n
[PROOFSTEP]
rwa [ih]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 0 ↔ n = 0
[PROOFSTEP]
rw [← cast_zero, cast_inj]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ¬n + 1 = 0
[PROOFSTEP]
exact n.succ_ne_zero
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 1 ↔ n = 1
[PROOFSTEP]
rw [← cast_one, cast_inj]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
h : Nat.AtLeastTwo n
⊢ ofNat n ≠ 1
[PROOFSTEP]
rw [← Nat.cast_eq_ofNat, ← @Nat.cast_one R, Ne.def, Nat.cast_inj]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
h : Nat.AtLeastTwo n
⊢ ¬n = 1
[PROOFSTEP]
exact ne_of_gt h.prop