-- Mathlib/Algebra/DirectSum/Ring.lean
theorem mul_eq_dfinsupp_sum [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (a a' : ⨁ i, A i) :
    a * a'
      = a.sum fun _ ai => a'.sum fun _ aj => DirectSum.of _ _ <| GradedMonoid.GMul.mul ai aj

Proof state:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (fun a b => ((toAddMonoid fun x => ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) a') = fun x ai =>
    DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
funext x

Result:
case h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b => ((toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip b) a') = fun ai =>
    DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Proof state:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ a * a' = DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
change mulHom _ a a' = _

Result:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ ((mulHom A) a) a' =
    DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Proof state:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (DFinsupp.sum a fun x => ⇑(toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) a' =
    DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
rw [AddMonoidHom.dfinsupp_sum_apply]

Result:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (DFinsupp.sum a fun a b => ((toAddMonoid fun x => ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) a') =
    DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Proof state:
case h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b => (DFinsupp.sum a' fun x_1 => ⇑((compHom (of A (x + x_1))).comp (gMulHom A)).flip) b) = fun ai =>
    DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
simp only [gMulHom, AddMonoidHom.dfinsupp_sum_apply, flip_apply, coe_comp, AddMonoidHom.coe_mk,
ZeroHom.coe_mk, Function.comp_apply, AddMonoidHom.compHom_apply_apply]

Result:
no goals

Proof state:
case h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b => ((toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip) a') b) = fun ai =>
    DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
erw [DFinsupp.sumAddHom_apply]

Result:
case h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b => (DFinsupp.sum a' fun x_1 => ⇑((compHom (of A (x + x_1))).comp (gMulHom A)).flip) b) = fun ai =>
    DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Proof state:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (DFinsupp.sum a fun a b => ((toAddMonoid fun x => ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) a') =
    DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
apply congrArg _

Result:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (fun a b => ((toAddMonoid fun x => ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) a') = fun x ai =>
    DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Proof state:
case h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b => ((toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip b) a') = fun ai =>
    DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
simp_rw [flip_apply]

Result:
case h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b => ((toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip) a') b) = fun ai =>
    DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Proof state:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ ((DFinsupp.sumAddHom fun x => (toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) a)
      a' =
    DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
erw [DFinsupp.sumAddHom_apply]

Result:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (DFinsupp.sum a fun x => ⇑(toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) a' =
    DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Proof state:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ ((mulHom A) a) a' =
    DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
rw [mulHom, toAddMonoid, DFinsupp.liftAddHom_apply]

Result:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ ((DFinsupp.sumAddHom fun x => (toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) a)
      a' =
    DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)