ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ mulHom A = AddMonoidHom.flip (mulHom A)
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ a * b = b * a
suffices mulHom A = (mulHom A).flip by
  rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_apply]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i),
    ↑(mulHom A) (↑(of (fun i => A i) i) y) = ↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) i) y)
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ mulHom A = AddMonoidHom.flip (mulHom A)
apply addHom_ext
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ↑(mulHom A) (↑(of (fun i => A i) ai) ax) = ↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) ai) ax)
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i),
    ↑(mulHom A) (↑(of (fun i => A i) i) y) = ↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) i) y)
intro ai ax
case H.H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ∀ (i : ι) (y : A i),
    ↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) i) y) =
      ↑(↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) i) y)
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ↑(mulHom A) (↑(of (fun i => A i) ai) ax) = ↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) ai) ax)
apply addHom_ext
case H.H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ ↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) bi) bx) =
    ↑(↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) bi) bx)
case H.H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ∀ (i : ι) (y : A i),
    ↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) i) y) =
      ↑(↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) i) y)
intro bi bx
case H.H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ ↑(of A (ai + bi)) (GradedMonoid.GMul.mul ax bx) = ↑(of A (bi + ai)) (GradedMonoid.GMul.mul bx ax)
case H.H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ ↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) bi) bx) =
    ↑(↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) bi) bx)
rw [AddMonoidHom.flip_apply, mulHom_of_of, mulHom_of_of]
no goals
case H.H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ ↑(of A (ai + bi)) (GradedMonoid.GMul.mul ax bx) = ↑(of A (bi + ai)) (GradedMonoid.GMul.mul bx ax)
exact of_eq_of_gradedMonoid_eq (GCommSemiring.mul_comm ⟨ai, ax⟩ ⟨bi, bx⟩)
no goals
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
this : mulHom A = AddMonoidHom.flip (mulHom A)
⊢ a * b = b * a
rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_apply]