-- Mathlib/Algebra/MonoidAlgebra/MapDomain.lean
theorem mapDomain_mul {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Mul α] [Mul α₂]
    {F : Type*} [FunLike F α α₂] [MulHomClass F α α₂] (f : F) (x y : MonoidAlgebra β α) :
    mapDomain f (x * y) = mapDomain f x * mapDomain f y

Proof state:
case e_g.h.h.H
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
x✝ : α₂
⊢ (sum y fun a_1 b_1 => Finsupp.single (f a * f a_1) (b * b_1)) x✝ =
    (sum (mapDomain (⇑f) y) fun a₂ b₂ => single (f a * a₂) (b * b₂)) x✝

Tactic:
rw [Finsupp.sum_mapDomain_index]

Result:
case e_g.h.h.H.h_zero
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
x✝ : α₂
⊢ ∀ (b_1 : α₂), single (f a * b_1) (b * 0) = 0

case e_g.h.h.H.h_add
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
x✝ : α₂
⊢ ∀ (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₂)

Proof state:
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
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₂)

Tactic:
rw [Finsupp.sum_mapDomain_index]

Result:
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
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
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
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
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
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₂)

Proof state:
case h_zero
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ ∀ (b : α₂), (sum (mapDomain (⇑f) y) fun a₂ b₂ => single (b * a₂) (0 * b₂)) = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
⊢ mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

Tactic:
simp_rw [mul_def, mapDomain_sum, mapDomain_single, map_mul]

Result:
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
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₂)

Proof state:
case e_g.h.h.H.h_zero
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
x✝ : α₂
⊢ ∀ (b_1 : α₂), single (f a * b_1) (b * 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
case e_g.h.h.H.h_add
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
x✝ : α₂
⊢ ∀ (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₂)

Tactic:
simp [mul_add]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
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₂)

Tactic:
congr

Result:
case e_g
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
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₂)

Proof state:
case e_g
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
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₂)

Tactic:
ext a b

Result:
case e_g.h.h.H
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : MulHomClass F α α₂
f : F
x y : MonoidAlgebra β α
a : α
b : β
x✝ : α₂
⊢ (sum y fun a_1 b_1 => Finsupp.single (f a * f a_1) (b * b_1)) x✝ =
    (sum (mapDomain (⇑f) y) fun a₂ b₂ => single (f a * a₂) (b * b₂)) x✝

Proof state:
case h_add
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Mul α
inst✝² : Mul α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
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₂)

Tactic:
simp [add_mul]

Result:
no goals