k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = ↑0 g'
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ x * of' k G g %ᵒᶠ g = 0
refine Finsupp.ext fun g' => ?_
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = 0
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = ↑0 g'
rw [Finsupp.zero_apply]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(x * of' k G g %ᵒᶠ g) (g + d) = 0

case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = 0
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = 0
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
no goals
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(x * of' k G g %ᵒᶠ g) (g + d) = 0
rw [modOf_apply_self_add]
case inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ¬∃ d, g' = d + g
case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = 0
rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, mul_single_apply_of_not_exists_add]
no goals
case inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ¬∃ d, g' = d + g
simpa only [add_comm] using h