k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ (sum x fun a b => sum y fun a_1 b_1 => Finsupp.single (↑f a * ↑f a_1) (b * b_1)) =
    sum (mapDomain (↑f) x) fun a₁ b₁ => sum (mapDomain (↑f) y) fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ mapDomain (↑f) (x * y) = mapDomain (↑f) x * mapDomain (↑f) y
simp_rw [mul_def, mapDomain_sum, mapDomain_single, map_mul]
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ (sum x fun a b => sum y fun a_1 b_1 => Finsupp.single (↑f a * ↑f a_1) (b * b_1)) =
    sum x fun a m => sum (mapDomain (↑f) y) fun a₂ b₂ => single (↑f a * a₂) (m * b₂)

case h_zero
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ ∀ (b : α₂), (sum (mapDomain (↑f) y) fun a₂ b₂ => single (b * a₂) (0 * b₂)) = 0

case h_add
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ ∀ (b : α₂) (m₁ m₂ : β),
    (sum (mapDomain (↑f) y) fun a₂ b₂ => single (b * a₂) ((m₁ + m₂) * b₂)) =
      (sum (mapDomain (↑f) y) fun a₂ b₂ => single (b * a₂) (m₁ * b₂)) +
        sum (mapDomain (↑f) y) fun a₂ b₂ => single (b * a₂) (m₂ * b₂)
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ (sum x fun a b => sum y fun a_1 b_1 => Finsupp.single (↑f a * ↑f a_1) (b * b_1)) =
    sum (mapDomain (↑f) x) fun a₁ b₁ => sum (mapDomain (↑f) y) fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)
rw [Finsupp.sum_mapDomain_index]
case e_g
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ (fun a b => sum y fun a_1 b_1 => Finsupp.single (↑f a * ↑f a_1) (b * b_1)) = fun a m =>
    sum (mapDomain (↑f) y) fun a₂ b₂ => single (↑f a * a₂) (m * b₂)
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ (sum x fun a b => sum y fun a_1 b_1 => Finsupp.single (↑f a * ↑f a_1) (b * b_1)) =
    sum x fun a m => sum (mapDomain (↑f) y) fun a₂ b₂ => single (↑f a * a₂) (m * b₂)
congr
case e_g.h.h
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
⊢ (sum y fun a_1 b_1 => Finsupp.single (↑f a * ↑f a_1) (b * b_1)) =
    sum (mapDomain (↑f) y) fun a₂ b₂ => single (↑f a * a₂) (b * b₂)
case e_g
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ (fun a b => sum y fun a_1 b_1 => Finsupp.single (↑f a * ↑f a_1) (b * b_1)) = fun a m =>
    sum (mapDomain (↑f) y) fun a₂ b₂ => single (↑f a * a₂) (m * b₂)
ext (a b)
case e_g.h.h.h_zero
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
⊢ ∀ (b_1 : α₂), single (↑f a * b_1) (b * 0) = 0

case e_g.h.h.h_add
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
⊢ ∀ (b_1 : α₂) (m₁ m₂ : β),
    single (↑f a * b_1) (b * (m₁ + m₂)) = single (↑f a * b_1) (b * m₁) + single (↑f a * b_1) (b * m₂)
case e_g.h.h
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
⊢ (sum y fun a_1 b_1 => Finsupp.single (↑f a * ↑f a_1) (b * b_1)) =
    sum (mapDomain (↑f) y) fun a₂ b₂ => single (↑f a * a₂) (b * b₂)
rw [Finsupp.sum_mapDomain_index]
no goals
case e_g.h.h.h_zero
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
⊢ ∀ (b_1 : α₂), single (↑f a * b_1) (b * 0) = 0
simp
no goals
case e_g.h.h.h_add
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
⊢ ∀ (b_1 : α₂) (m₁ m₂ : β),
    single (↑f a * b_1) (b * (m₁ + m₂)) = single (↑f a * b_1) (b * m₁) + single (↑f a * b_1) (b * m₂)
simp [mul_add]
no goals
case h_zero
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ ∀ (b : α₂), (sum (mapDomain (↑f) y) fun a₂ b₂ => single (b * a₂) (0 * b₂)) = 0
simp
no goals
case h_add
k : Type u₁
G : Type u₂
R : Type ?u.413727
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : Mul α
inst✝¹ : Mul α₂
F : Type u_4
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ ∀ (b : α₂) (m₁ m₂ : β),
    (sum (mapDomain (↑f) y) fun a₂ b₂ => single (b * a₂) ((m₁ + m₂) * b₂)) =
      (sum (mapDomain (↑f) y) fun a₂ b₂ => single (b * a₂) (m₁ * b₂)) +
        sum (mapDomain (↑f) y) fun a₂ b₂ => single (b * a₂) (m₂ * b₂)
simp [add_mul]