-- Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean
theorem toDirectSum_mul [DecidableEq ι] [AddMonoid ι] [Semiring M] (f g : AddMonoidAlgebra M ι) :
    (f * g).toDirectSum = f.toDirectSum * g.toDirectSum

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : M[ι]
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ to_hom (f * g) = to_hom f * to_hom g

Tactic:
revert f g

Result:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (f g : M[ι]), to_hom (f * g) = to_hom f * to_hom g

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : M[ι]
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ (f * g).toDirectSum = f.toDirectSum * g.toDirectSum

Tactic:
show to_hom (f * g) = to_hom f * to_hom g

Result:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : M[ι]
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ to_hom (f * g) = to_hom f * to_hom g

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : M[ι]
⊢ (f * g).toDirectSum = f.toDirectSum * g.toDirectSum

Tactic:
let to_hom : AddMonoidAlgebra M ι →+ ⨁ _ : ι, M :=
{ toFun := toDirectSum
  map_zero' := toDirectSum_zero
  map_add' := toDirectSum_add }

Result:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : M[ι]
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ (f * g).toDirectSum = f.toDirectSum * g.toDirectSum

Proof state:
case H.h.H.h
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
xi : ι
xv : M
yi : ι
yv : M
⊢ ((((AddMonoidHom.mul.compr₂ to_hom).comp (singleAddHom xi)) xv).comp (singleAddHom yi)) yv =
    (((((AddMonoidHom.mul.comp to_hom).compl₂ to_hom).comp (singleAddHom xi)) xv).comp (singleAddHom yi)) yv

Tactic:
simp [to_hom, AddMonoidAlgebra.single_mul_single, DirectSum.of_mul_of]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ AddMonoidHom.mul.compr₂ to_hom = (AddMonoidHom.mul.comp to_hom).compl₂ to_hom

Tactic:
ext xi xv yi yv : 4

Result:
case H.h.H.h
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
xi : ι
xv : M
yi : ι
yv : M
⊢ ((((AddMonoidHom.mul.compr₂ to_hom).comp (singleAddHom xi)) xv).comp (singleAddHom yi)) yv =
    (((((AddMonoidHom.mul.comp to_hom).compl₂ to_hom).comp (singleAddHom xi)) xv).comp (singleAddHom yi)) yv

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (f g : M[ι]), to_hom (f * g) = to_hom f * to_hom g

Tactic:
rw [AddMonoidHom.map_mul_iff]

Result:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ AddMonoidHom.mul.compr₂ to_hom = (AddMonoidHom.mul.comp to_hom).compl₂ to_hom