ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ↑(↑(toAddMonoid fun x =>
              AddMonoidHom.flip
                (toAddMonoid fun x_1 => AddMonoidHom.flip (AddMonoidHom.comp (↑compHom (of A (x + x_1))) (gMulHom A))))
          (↑(of A i) a))
      (↑(of A j) b) =
    ↑(of A (i + j)) (GradedMonoid.GMul.mul a b)
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ↑(↑(mulHom A) (↑(of A i) a)) (↑(of A j) b) = ↑(of A (i + j)) (GradedMonoid.GMul.mul a b)
unfold mulHom
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ↑(↑(↑compHom (of A (i + j))) (↑(gMulHom A) a)) b = ↑(of A (i + j)) (GradedMonoid.GMul.mul a b)
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ↑(↑(toAddMonoid fun x =>
              AddMonoidHom.flip
                (toAddMonoid fun x_1 => AddMonoidHom.flip (AddMonoidHom.comp (↑compHom (of A (x + x_1))) (gMulHom A))))
          (↑(of A i) a))
      (↑(of A j) b) =
    ↑(of A (i + j)) (GradedMonoid.GMul.mul a b)
simp only [toAddMonoid_of, flip_apply, coe_comp, Function.comp_apply]
no goals
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ↑(↑(↑compHom (of A (i + j))) (↑(gMulHom A) a)) b = ↑(of A (i + j)) (GradedMonoid.GMul.mul a b)
rfl