k : Type u₁
G : Type u₂
R : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : Semiring R
g_hom : Type u_1
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : MonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → Commute (↑f (↑b x)) (↑g y)
⊢ ↑(liftNC ↑f ↑g) (a * b) = ↑(liftNC ↑f ↑g) (sum a single) * ↑(liftNC ↑f ↑g) (sum b single)
k : Type u₁
G : Type u₂
R : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : Semiring R
g_hom : Type u_1
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : MonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → Commute (↑f (↑b x)) (↑g y)
⊢ ↑(liftNC ↑f ↑g) (a * b) = ↑(liftNC ↑f ↑g) a * ↑(liftNC ↑f ↑g) b
conv_rhs => rw [← sum_single a, ← sum_single b]
k : Type u₁
G : Type u₂
R : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : Semiring R
g_hom : Type u_1
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : MonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → Commute (↑f (↑b x)) (↑g y)
⊢ (sum a fun a b_1 => sum b fun a_1 b => ↑↑f (b_1 * b) * ↑g (a * a_1)) =
    sum a fun a c => sum b fun a_1 c_1 => ↑↑f c * ↑g a * (↑↑f c_1 * ↑g a_1)
k : Type u₁
G : Type u₂
R : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : Semiring R
g_hom : Type u_1
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : MonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → Commute (↑f (↑b x)) (↑g y)
⊢ ↑(liftNC ↑f ↑g) (a * b) = ↑(liftNC ↑f ↑g) (sum a single) * ↑(liftNC ↑f ↑g) (sum b single)
simp_rw [mul_def, map_finsupp_sum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]
k : Type u₁
G : Type u₂
R : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : Semiring R
g_hom : Type u_1
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : MonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → Commute (↑f (↑b x)) (↑g y)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ (fun a_1 b => ↑↑f (↑a y * b) * ↑g (y * a_1)) x (↑b x) = (fun a_1 c => ↑↑f (↑a y) * ↑g y * (↑↑f c * ↑g a_1)) x (↑b x)
k : Type u₁
G : Type u₂
R : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : Semiring R
g_hom : Type u_1
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : MonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → Commute (↑f (↑b x)) (↑g y)
⊢ (sum a fun a b_1 => sum b fun a_1 b => ↑↑f (b_1 * b) * ↑g (a * a_1)) =
    sum a fun a c => sum b fun a_1 c_1 => ↑↑f c * ↑g a * (↑↑f c_1 * ↑g a_1)
refine Finset.sum_congr rfl fun y hy => Finset.sum_congr rfl fun x _hx => ?_
no goals
k : Type u₁
G : Type u₂
R : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : Semiring R
g_hom : Type u_1
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : MonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → Commute (↑f (↑b x)) (↑g y)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ (fun a_1 b => ↑↑f (↑a y * b) * ↑g (y * a_1)) x (↑b x) = (fun a_1 c => ↑↑f (↑a y) * ↑g y * (↑↑f c * ↑g a_1)) x (↑b x)
simp [mul_assoc, (h_comm hy).left_comm]