-- Mathlib/Algebra/DirectSum/Ring.lean
theorem mul_assoc (a b c : ⨁ i, A i) : a * b * c = a * (b * c)

Proof state:
case H.h.H.h.H.h
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ ((mulHom A) (((mulHom A) ((of A ai) ax)) ((of A bi) bx))) ((of A ci) cx) =
    ((mulHom A) ((of A ai) ax)) (((mulHom A) ((of A bi) bx)) ((of A ci) cx))

Tactic:
simp_rw [mulHom_of_of]

Result:
case H.h.H.h.H.h
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ (of A (ai + bi + ci)) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul ax bx) cx) =
    (of A (ai + (bi + ci))) (GradedMonoid.GMul.mul ax (GradedMonoid.GMul.mul bx cx))

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
⊢ (compHom (mulHom A)).comp (mulHom A) = ((compHom flipHom) ((compHom (mulHom A).flip).comp (mulHom A))).flip

Tactic:
ext ai ax bi bx ci cx : 6

Result:
case H.h.H.h.H.h
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ (((((((compHom (mulHom A)).comp (mulHom A)).comp (of A ai)) ax).comp (of A bi)) bx).comp (of A ci)) cx =
    (((((((compHom flipHom) ((compHom (mulHom A).flip).comp (mulHom A))).flip.comp (of A ai)) ax).comp (of A bi))
            bx).comp
        (of A ci))
      cx

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
this : (compHom (mulHom A)).comp (mulHom A) = ((compHom flipHom) ((compHom (mulHom A).flip).comp (mulHom A))).flip
⊢ a * b * c = a * (b * c)

Tactic:
simpa only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, flip_apply,
  AddMonoidHom.flipHom_apply]
  using DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this a) b) c

Result:
no goals

Proof state:
case H.h.H.h.H.h
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ (((((((compHom (mulHom A)).comp (mulHom A)).comp (of A ai)) ax).comp (of A bi)) bx).comp (of A ci)) cx =
    (((((((compHom flipHom) ((compHom (mulHom A).flip).comp (mulHom A))).flip.comp (of A ai)) ax).comp (of A bi))
            bx).comp
        (of A ci))
      cx

Tactic:
dsimp only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, flip_apply,
  AddMonoidHom.flipHom_apply]

Result:
case H.h.H.h.H.h
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ ((mulHom A) (((mulHom A) ((of A ai) ax)) ((of A bi) bx))) ((of A ci) cx) =
    ((mulHom A) ((of A ai) ax)) (((mulHom A) ((of A bi) bx)) ((of A ci) cx))

Proof state:
case H.h.H.h.H.h
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ (of A (ai + bi + ci)) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul ax bx) cx) =
    (of A (ai + (bi + ci))) (GradedMonoid.GMul.mul ax (GradedMonoid.GMul.mul bx cx))

Tactic:
exact of_eq_of_gradedMonoid_eq (_root_.mul_assoc (GradedMonoid.mk ai ax) ⟨bi, bx⟩ ⟨ci, cx⟩)

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
⊢ a * b * c = a * (b * c)

Tactic:
suffices (mulHom A).compHom.comp (mulHom A) =
    (AddMonoidHom.compHom flipHom <| (mulHom A).flip.compHom.comp (mulHom A)).flip by
    simpa only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, flip_apply,
      AddMonoidHom.flipHom_apply]
      using DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this a) b) c

Result:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
⊢ (compHom (mulHom A)).comp (mulHom A) = ((compHom flipHom) ((compHom (mulHom A).flip).comp (mulHom A))).flip