k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ (sum x fun x v => if x * g = g' then v * r else 0) = 0

k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ (sum x fun x v => if x * g = g' then v * 0 else 0) = 0
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ ↑(x * single g r) g' = 0
rw [mul_apply, Finsupp.sum_comm, Finsupp.sum_single_index]
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ (sum x fun x v => if x * g = g' then v * 0 else 0) = 0

k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ (sum x fun x v => if x * g = g' then v * r else 0) = 0
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ (sum x fun x v => if x * g = g' then v * r else 0) = 0

k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ (sum x fun x v => if x * g = g' then v * 0 else 0) = 0
swap
no goals
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ (sum x fun x v => if x * g = g' then v * 0 else 0) = 0
simp_rw [Finsupp.sum, MulZeroClass.mul_zero, ite_self, Finset.sum_const_zero]
case h
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ ∀ (x_1 : G), x_1 ∈ x.support → (fun x v => if x * g = g' then v * r else 0) x_1 (↑x x_1) = 0
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ (sum x fun x v => if x * g = g' then v * r else 0) = 0
apply Finset.sum_eq_zero
case h
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ ∀ (x_1 : G), x_1 ∈ x.support → x_1 * g = g' → ↑x x_1 * r = 0
case h
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ ∀ (x_1 : G), x_1 ∈ x.support → (fun x v => if x * g = g' then v * r else 0) x_1 (↑x x_1) = 0
simp_rw [ite_eq_right_iff]
case h
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g : G
x : MonoidAlgebra k G
g'' : G
_hg'' : g'' ∈ x.support
h : ¬∃ d, g'' * g = d * g
⊢ ↑x g'' * r = 0
case h
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g g' : G
x : MonoidAlgebra k G
h : ¬∃ d, g' = d * g
⊢ ∀ (x_1 : G), x_1 ∈ x.support → x_1 * g = g' → ↑x x_1 * r = 0
rintro g'' _hg'' rfl
case h.h
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g : G
x : MonoidAlgebra k G
g'' : G
_hg'' : g'' ∈ x.support
h : ¬∃ d, g'' * g = d * g
⊢ False
case h
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g : G
x : MonoidAlgebra k G
g'' : G
_hg'' : g'' ∈ x.support
h : ¬∃ d, g'' * g = d * g
⊢ ↑x g'' * r = 0
exfalso
no goals
case h.h
k : Type u₁
G : Type u₂
R : Type ?u.506603
inst✝¹ : Semiring k
inst✝ : Mul G
r : k
g : G
x : MonoidAlgebra k G
g'' : G
_hg'' : g'' ∈ x.support
h : ¬∃ d, g'' * g = d * g
⊢ False
exact h ⟨_, rfl⟩