[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
a b : R
⊢ OneHom.toFun
      { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
        map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
      (a * b) =
    OneHom.toFun
        { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
          map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
        a *
      OneHom.toFun
        { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
          map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
        b
[PROOFSTEP]
simp only [AddMonoidHom.comp_apply]
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
a b : R
⊢ ↑(of A 0) (↑GAlgebra.toFun (a * b)) = ↑(of A 0) (↑GAlgebra.toFun a) * ↑(of A 0) (↑GAlgebra.toFun b)
[PROOFSTEP]
rw [of_mul_of]
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
a b : R
⊢ ↑(of A 0) (↑GAlgebra.toFun (a * b)) = ↑(of A (0 + 0)) (GradedMonoid.GMul.mul (↑GAlgebra.toFun a) (↑GAlgebra.toFun b))
[PROOFSTEP]
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.map_mul a b)
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                    map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) },
                map_mul' :=
                  (_ :
                    ∀ (a b : R),
                      OneHom.toFun
                          { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                            map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            a *
                          OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            b) },
            map_zero' := (_ : ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) 0 = 0),
            map_add' :=
              (_ :
                ∀ (a b : R),
                  ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) (a + b) =
                    ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) a + ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) b) }
        r *
      x =
    x *
      ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                    map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) },
                map_mul' :=
                  (_ :
                    ∀ (a b : R),
                      OneHom.toFun
                          { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                            map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            a *
                          OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            b) },
            map_zero' := (_ : ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) 0 = 0),
            map_add' :=
              (_ :
                ∀ (a b : R),
                  ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) (a + b) =
                    ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) a + ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) b) }
        r
[PROOFSTEP]
change AddMonoidHom.mul (DirectSum.of _ _ _) x = AddMonoidHom.mul.flip (DirectSum.of _ _ _) x
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ ↑(↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) x =
    ↑(↑(AddMonoidHom.flip AddMonoidHom.mul) (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) x
[PROOFSTEP]
apply FunLike.congr_fun _ x
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ ↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r)) =
    ↑(AddMonoidHom.flip AddMonoidHom.mul) (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))
[PROOFSTEP]
ext i xi : 2
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(AddMonoidHom.comp (↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) (of (fun i => A i) i)) xi =
    ↑(AddMonoidHom.comp (↑(AddMonoidHom.flip AddMonoidHom.mul) (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r)))
          (of (fun i => A i) i))
      xi
[PROOFSTEP]
dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.mul_apply, AddMonoidHom.flip_apply]
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(of (fun i => A i) 0) (↑GAlgebra.toFun r) * ↑(of (fun i => A i) i) xi =
    ↑(of (fun i => A i) i) xi * ↑(of (fun i => A i) 0) (↑GAlgebra.toFun r)
[PROOFSTEP]
rw [of_mul_of, of_mul_of]
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(of (fun i => A i) (0 + i)) (GradedMonoid.GMul.mul (↑GAlgebra.toFun r) xi) =
    ↑(of (fun i => A i) (i + 0)) (GradedMonoid.GMul.mul xi (↑GAlgebra.toFun r))
[PROOFSTEP]
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.commutes r ⟨i, xi⟩)
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ r • x =
    ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                    map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) },
                map_mul' :=
                  (_ :
                    ∀ (a b : R),
                      OneHom.toFun
                          { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                            map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            a *
                          OneHom.toFun
                            { toFun := ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun),
                              map_one' := (_ : ↑(of A 0) (↑GAlgebra.toFun 1) = ↑(of A 0) GradedMonoid.GOne.one) }
                            b) },
            map_zero' := (_ : ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) 0 = 0),
            map_add' :=
              (_ :
                ∀ (a b : R),
                  ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) (a + b) =
                    ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) a + ↑(AddMonoidHom.comp (of A 0) GAlgebra.toFun) b) }
        r *
      x
[PROOFSTEP]
change DistribMulAction.toAddMonoidHom _ r x = AddMonoidHom.mul (DirectSum.of _ _ _) x
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ ↑(DistribMulAction.toAddMonoidHom ((fun x => ⨁ (i : ι), A i) r) r) x =
    ↑(↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) x
[PROOFSTEP]
apply FunLike.congr_fun _ x
[GOAL]
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
⊢ DistribMulAction.toAddMonoidHom ((fun x => ⨁ (i : ι), A i) r) r =
    ↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))
[PROOFSTEP]
ext i xi : 2
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(AddMonoidHom.comp (DistribMulAction.toAddMonoidHom ((fun x => ⨁ (i : ι), A i) r) r) (of (fun i => A i) i)) xi =
    ↑(AddMonoidHom.comp (↑AddMonoidHom.mul (↑(of (fun i => A i) 0) (↑GAlgebra.toFun r))) (of (fun i => A i) i)) xi
[PROOFSTEP]
dsimp only [AddMonoidHom.comp_apply, DistribMulAction.toAddMonoidHom_apply, AddMonoidHom.mul_apply]
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ r • ↑(of (fun i => A i) i) xi = ↑(of (fun i => A i) 0) (↑GAlgebra.toFun r) * ↑(of (fun i => A i) i) xi
[PROOFSTEP]
rw [DirectSum.of_mul_of, ← of_smul]
[GOAL]
case H.h
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
r : R
x : (fun x => ⨁ (i : ι), A i) r
i : ι
xi : A i
⊢ ↑(of (fun i => A i) i) (r • xi) = ↑(of (fun i => A i) (0 + i)) (GradedMonoid.GMul.mul (↑GAlgebra.toFun r) xi)
[PROOFSTEP]
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.smul_def r ⟨i, xi⟩)
