-- Mathlib/Algebra/DirectSum/Internal.lean
theorem coe_mul_apply_eq_dfinsupp_sum [AddMonoid ι] [SetLike.GradedMonoid A]
    [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (r r' : ⨁ i, A i) (n : ι) :
    ((r * r') n : R) = r.sum fun i ri => r'.sum fun j rj => if i + j = n then (ri * rj : R)
      else 0

Proof state:
case e_f.h.e_f.h
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
⊢ ↑(((of (fun i => ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) =
    if x✝¹ + x✝ = n then ↑(r x✝¹) * ↑(r' x✝) else 0

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
h : x✝¹ + x✝ = n
⊢ ↑(((of (fun i => ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = ↑(r x✝¹) * ↑(r' x✝)

case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑(((of (fun i => ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = 0

Proof state:
case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
x✝¹ x✝ : ι
⊢ ↑(((of (fun i => ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) (x✝¹ + x✝)) = ↑(r x✝¹) * ↑(r' x✝)

Tactic:
rw [of_eq_same]

Result:
case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
x✝¹ x✝ : ι
⊢ ↑(GradedMonoid.GMul.mul (r x✝¹) (r' x✝)) = ↑(r x✝¹) * ↑(r' x✝)

Proof state:
case e_f.h
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ ∑ i ∈ DFinsupp.support r', ↑(((of (fun i => ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n) =
    (fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)

Tactic:
congr

Result:
case e_f.h.e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ (fun i => ↑(((of (fun i => ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n)) = fun i =>
    (fun j rj => if x✝ + j = n then ↑(r x✝) * ↑rj else 0) i (r' i)

Proof state:
case e_f.h
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ ↑((DFinsupp.sum r' fun x aj => (of (fun i => ↥(A i)) (x✝ + x)) (GradedMonoid.GMul.mul (r x✝) aj)) n) =
    (fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)

Tactic:
rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finset_sum]

Result:
case e_f.h
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ ∑ i ∈ DFinsupp.support r', ↑(((of (fun i => ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n) =
    (fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)

Proof state:
case e_f.h.e_f.h
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
⊢ ↑(((of (fun i => ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) =
    (fun j rj => if x✝¹ + j = n then ↑(r x✝¹) * ↑rj else 0) x✝ (r' x✝)

Tactic:
dsimp only

Result:
case e_f.h.e_f.h
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
⊢ ↑(((of (fun i => ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) =
    if x✝¹ + x✝ = n then ↑(r x✝¹) * ↑(r' x✝) else 0

Proof state:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((r * r') n) = DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0

Tactic:
rw [mul_eq_dfinsupp_sum]

Result:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((DFinsupp.sum r fun x ai =>
          DFinsupp.sum r' fun x_1 aj => (of (fun i => ↥(A i)) (x + x_1)) (GradedMonoid.GMul.mul ai aj))
        n) =
    DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0

Proof state:
case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑(((of (fun i => ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = 0

Tactic:
rw [of_eq_of_ne _ _ _ h]

Result:
case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑0 = 0

Proof state:
case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑0 = 0

Tactic:
rfl

Result:
no goals