[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : AddMonoidAlgebra M ι
⊢ toDirectSum (f * g) = toDirectSum f * toDirectSum g
[PROOFSTEP]
let to_hom : AddMonoidAlgebra M ι →+ ⨁ _ : ι, M :=
  { toFun := toDirectSum
    map_zero' := toDirectSum_zero
    map_add' := toDirectSum_add }
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : AddMonoidAlgebra M ι
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
⊢ toDirectSum (f * g) = toDirectSum f * toDirectSum g
[PROOFSTEP]
show to_hom (f * g) = to_hom f * to_hom g
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : AddMonoidAlgebra M ι
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
⊢ ↑to_hom (f * g) = ↑to_hom f * ↑to_hom g
[PROOFSTEP]
let _ : NonUnitalNonAssocSemiring (ι →₀ M) := AddMonoidAlgebra.nonUnitalNonAssocSemiring
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : AddMonoidAlgebra M ι
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
⊢ ↑to_hom (f * g) = ↑to_hom f * ↑to_hom g
[PROOFSTEP]
revert f g
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
⊢ ∀ (f g : AddMonoidAlgebra M ι), ↑to_hom (f * g) = ↑to_hom f * ↑to_hom g
[PROOFSTEP]
rw [AddMonoidHom.map_mul_iff]
  -- porting note: does not find `addHom_ext'`, was `ext (xi xv yi yv) : 4`
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul to_hom = AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul to_hom) to_hom
[PROOFSTEP]
refine Finsupp.addHom_ext' fun xi => AddMonoidHom.ext fun xv => ?_
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
⊢ ↑(AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul to_hom) (Finsupp.singleAddHom xi)) xv =
    ↑(AddMonoidHom.comp (AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul to_hom) to_hom)
          (Finsupp.singleAddHom xi))
      xv
[PROOFSTEP]
refine Finsupp.addHom_ext' fun yi => AddMonoidHom.ext fun yv => ?_
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ ↑(AddMonoidHom.comp (↑(AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul to_hom) (Finsupp.singleAddHom xi)) xv)
          (Finsupp.singleAddHom yi))
      yv =
    ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp (AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul to_hom) to_hom)
                (Finsupp.singleAddHom xi))
            xv)
          (Finsupp.singleAddHom yi))
      yv
[PROOFSTEP]
dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.compl₂_apply, AddMonoidHom.compr₂_apply, AddMonoidHom.mul_apply,
  Finsupp.singleAddHom_apply]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ ↑{ toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
          map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
      (Finsupp.single xi xv * Finsupp.single yi yv) =
    ↑{ toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
            map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
        (Finsupp.single xi xv) *
      ↑{ toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
            map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
        (Finsupp.single yi yv)
[PROOFSTEP]
simp only [AddMonoidHom.coe_mk, ZeroHom.coe_mk, toDirectSum_single]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ toDirectSum (Finsupp.single xi xv * Finsupp.single yi yv) =
    ↑(DirectSum.of (fun i => M) xi) xv * ↑(DirectSum.of (fun i => M) yi) yv
[PROOFSTEP]
erw [AddMonoidAlgebra.single_mul_single, AddMonoidHom.coe_mk, ZeroHom.coe_mk, AddMonoidAlgebra.toDirectSum_single]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ ↑(DirectSum.of (fun i => M) (xi + yi)) (xv * yv) = DFinsupp.single xi xv * ↑(DirectSum.of (fun i => M) yi) yv
[PROOFSTEP]
simp only [AddMonoidHom.coe_comp, AddMonoidHom.coe_mul, AddMonoidHom.coe_mk, ZeroHom.coe_mk, Function.comp_apply,
  toDirectSum_single, AddMonoidHom.id_apply, Finsupp.singleAddHom_apply, AddMonoidHom.coe_mulLeft]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : AddMonoidAlgebra M ι →+ ⨁ (x : ι), M :=
  { toZeroHom := { toFun := toDirectSum, map_zero' := (_ : toDirectSum 0 = 0) },
    map_add' := (_ : ∀ (f g : AddMonoidAlgebra M ι), toDirectSum (f + g) = toDirectSum f + toDirectSum g) }
x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring
xi : ι
xv : M
yi : ι
yv : M
⊢ ↑(DirectSum.of (fun i => M) (xi + yi)) (xv * yv) = DFinsupp.single xi xv * ↑(DirectSum.of (fun i => M) yi) yv
[PROOFSTEP]
erw [DirectSum.of_mul_of, Mul.gMul_mul]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ toAddMonoidAlgebra (f * g) = toAddMonoidAlgebra f * toAddMonoidAlgebra g
[PROOFSTEP]
apply_fun AddMonoidAlgebra.toDirectSum
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ AddMonoidAlgebra.toDirectSum (toAddMonoidAlgebra (f * g)) =
    AddMonoidAlgebra.toDirectSum (toAddMonoidAlgebra f * toAddMonoidAlgebra g)
[PROOFSTEP]
simp
[GOAL]
case inj
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.Injective AddMonoidAlgebra.toDirectSum
[PROOFSTEP]
apply Function.LeftInverse.injective
[GOAL]
case inj.a
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.LeftInverse ?inj.g AddMonoidAlgebra.toDirectSum
case inj.g
ι : Type u_1
R : Type u_2
M : Type u_3
A : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (⨁ (x : ι), M) → AddMonoidAlgebra M ι
[PROOFSTEP]
apply AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra
