awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Finsupp
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : DecidableEq ι
N : Type u_2
inst_4 : AddCommMonoid N
inst_5 : Module R N
ε : M →ₗ[R] N
m : ι →₀ M
i : ι
⊢ (((lmap (M := fun (x : ι) ↦ M) (N := fun (x : ι) ↦ N) fun (x : ι) ↦ ε : (a : ⨁ (i : ι), M) → ⨁ (i : ι), N)
            ((finsuppLEquivDirectSum R M ι : (a : ι →₀ M) → ⨁ (x : ι), M) m) :
          ⨁ (i : ι), N) :
        (a : ι) → N)
      i =
    (((finsuppLEquivDirectSum R N ι : (a : ι →₀ N) → ⨁ (x : ι), N) (Finsupp.mapRange (⇑ε : (a : M) → N) ⋯ m) :
          ⨁ (x : ι), N) :
        (a : ι) → N)
      i

Tactic:
rfl
-- Module: Mathlib.Algebra.DirectSum.Idempotents
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
x : R
i : I
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₂ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑(x • ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₃ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((HSMul.hSMul (β := ⨁ (i : I), ↥(V i)) x ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1) : (a : I) → ↥(V a)) i) :
      R)
rw₄ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (HSMul.hSMul (β := R) x 1) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a))
          i) :
      R)
rw₅ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (x * 1) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R)
rw₆ rw₇ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R)
⊢ (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x * idempotent V i

Tactic:
rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]

Premises used: Submodule.coe_smul, DirectSum.idempotent, DirectSum.smul_apply, smul_eq_mul, mul_one, DirectSum.decompose_smul
-- Module: Mathlib.Algebra.DirectSum.Idempotents
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
i : I
rw : idempotent V i * idempotent V i = idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    idempotent V i
rw₂ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i))
                (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          i) :
      R) =
    (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₃ :
  (↑(((((of.{u_2, u_1} (fun (i : I) ↦ ↥(V i)) i : ↥(V i) →+ ⨁ (i : I), ↥(V i)) : (a : ↥(V i)) → ⨁ (i : I), ↥(V i))
                (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          i) :
      R) =
    (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₄ rw₅ :
  (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) =
    (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
⊢ IsIdempotentElem (idempotent V i)

Tactic:
rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]

Premises used: DirectSum.decompose_eq_mul_idempotent, DirectSum.of_eq_same, IsIdempotentElem, DirectSum.idempotent, DirectSum.decompose_coe
-- Module: Mathlib.Algebra.DirectSum.Idempotents
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
i j : I
hij : i ≠ j
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) j) : R) = 0
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i))
                (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          j) :
      R) =
    0
rw₂ :
  (↑(((((of.{u_2, u_1} (fun (i : I) ↦ ↥(V i)) i : ↥(V i) →+ ⨁ (i : I), ↥(V i)) : (a : ↥(V i)) → ⨁ (i : I), ↥(V i))
                (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          j) :
      R) =
    0
rw₃ : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
rw₄ rw₅ : Eq.{u_1 + 1} (α := R) 0 0
⊢ idempotent V i * idempotent V j = 0

Tactic:
rw [← decompose_eq_mul_idempotent, idempotent, decompose_coe,
      of_eq_of_ne (h := hij.symm), Submodule.coe_zero]

Premises used: DirectSum.decompose_eq_mul_idempotent, Ne.symm, Submodule.coe_zero, DirectSum.idempotent, DirectSum.decompose_coe, DirectSum.of_eq_of_ne
-- Module: Mathlib.Algebra.DirectSum.Idempotents
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
a :
  Eq (α := ⨁ (i : I), ↥(V i)) ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (∑ i : I, idempotent V i))
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1)
⊢ Eq.{u_1 + 1} (α := R) (∑ i : I, idempotent V i) 1

Tactic:
apply (decompose V).injective

Premises used: Equiv.injective, DirectSum.decompose
-- Module: Mathlib.Algebra.DirectSum.Idempotents
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
⊢ Eq (α := ⨁ (i : I), ↥(V i)) ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (∑ i : I, idempotent V i))
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1)

Tactic:
DFunLike.ext _ _ fun i ↦ ?_

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.DirectSum.Idempotents
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
a :
  ∀ (i : I),
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (∑ i : I, idempotent V i) : (a : I) → ↥(V a)) i =
      ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i
⊢ Eq (α := ⨁ (i : I), ↥(V i)) ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (∑ i : I, idempotent V i))
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1)

Tactic:
refine DFunLike.ext _ _ fun i ↦ ?_

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.DirectSum.Idempotents
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
i : I
a :
  ∑ a : I, (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V a) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i =
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i
⊢ ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (∑ i : I, idempotent V i) : (a : I) → ↥(V a)) i =
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i

Tactic:
rw [decompose_sum, DFinsupp.finsetSum_apply]

Premises used: DFinsupp.finsetSum_apply, DirectSum.decompose_sum
-- Module: Mathlib.Algebra.DirectSum.Idempotents
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
i : I
⊢ ∑ a : I, (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V a) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i =
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i

Tactic:
simp [idempotent, of_apply]

Premises used: DirectSum.of_apply, DirectSum.idempotent
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
S : Type u_3
R : Type u_4
inst : Zero ι
inst_1 : CommSemiring S
inst_2 : Semiring R
inst_3 : Algebra S R
A : ι → Submodule S R
inst_4 : GradedOne A
s : S
rw : HSMul.hSMul (β := R) s 1 ∈ A 0
⊢ Membership.mem (α := R) (A 0) ((algebraMap S R : (a : S) → R) s : R)

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
S : Type u_3
R : Type u_4
inst : Zero ι
inst_1 : CommSemiring S
inst_2 : Semiring R
inst_3 : Algebra S R
A : ι → Submodule S R
inst_4 : GradedOne A
s : S
⊢ HSMul.hSMul (β := R) s 1 ∈ A 0

Tactic:
(A 0).smul_mem s <| SetLike.one_mem_graded _

Premises used: Set.Mem, SetLike.one_mem_graded, OfNat.ofNat, Submodule.smul_mem
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
S : Type u_3
R : Type u_4
inst : Zero ι
inst_1 : CommSemiring S
inst_2 : Semiring R
inst_3 : Algebra S R
A : ι → Submodule S R
inst_4 : GradedOne A
s : S
⊢ HSMul.hSMul (β := R) s 1 ∈ A 0

Tactic:
exact (A 0).smul_mem s <| SetLike.one_mem_graded _

Premises used: SetLike.one_mem_graded, OfNat.ofNat, Submodule.smul_mem
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
zero : 0 ∈ A 0
⊢ (↑0 : R) ∈ A 0

Tactic:
rw [Nat.cast_zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
⊢ 0 ∈ A 0

Tactic:
zero_mem (A 0)

Premises used: ZeroMemClass.zero_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
⊢ 0 ∈ A 0

Tactic:
exact zero_mem (A 0)

Premises used: ZeroMemClass.zero_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
n : ℕ
n_ih : (↑n : R) ∈ A 0
succ : HAdd.hAdd (α := R) (↑n : R) 1 ∈ A 0
⊢ (↑(n + 1) : R) ∈ A 0

Tactic:
rw [Nat.cast_succ]

Premises used: Nat.cast_succ
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
n : ℕ
n_ih : (↑n : R) ∈ A 0
⊢ HAdd.hAdd (α := R) (↑n : R) 1 ∈ A 0

Tactic:
add_mem n_ih (SetLike.one_mem_graded _)

Premises used: SetLike.one_mem_graded, AddMemClass.add_mem
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
n : ℕ
n_ih : (↑n : R) ∈ A 0
⊢ HAdd.hAdd (α := R) (↑n : R) 1 ∈ A 0

Tactic:
exact add_mem n_ih (SetLike.one_mem_graded _)

Premises used: SetLike.one_mem_graded, AddMemClass.add_mem
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
n : ℕ
zero : (↑0 : R) ∈ A 0
succ : ∀ (n : ℕ) (n_ih : (↑n : R) ∈ A 0), (↑(n + 1) : R) ∈ A 0
⊢ (↑n : R) ∈ A 0

Tactic:
induction n with
  | zero =>
    rw [Nat.cast_zero]
    exact zero_mem (A 0)
  | succ _ n_ih =>
    rw [Nat.cast_succ]
    exact add_mem n_ih (SetLike.one_mem_graded _)

Premises used: Nat.cast_succ, ZeroMemClass.zero_mem, Nat.cast_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
z : ℤ
ofNat : ∀ (a : ℕ), (↑(Int.ofNat a) : R) ∈ A 0
negSucc : ∀ (a : ℕ), (↑(Int.negSucc a) : R) ∈ A 0
⊢ (↑z : R) ∈ A 0

Tactic:
cases z
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
a : ℕ
ofNat : (↑a : R) ∈ A 0
⊢ (↑(Int.ofNat a) : R) ∈ A 0

Tactic:
rw [Int.ofNat_eq_natCast, Int.cast_natCast]

Premises used: Int.cast_natCast, Int.ofNat_eq_natCast
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
a : ℕ
⊢ (↑a : R) ∈ A 0

Tactic:
SetLike.natCast_mem_graded _ _

Premises used: SetLike.natCast_mem_graded
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
a : ℕ
⊢ (↑a : R) ∈ A 0

Tactic:
exact SetLike.natCast_mem_graded _ _

Premises used: SetLike.natCast_mem_graded
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
a : ℕ
negSucc : -(↑(a + 1) : R) ∈ A 0
⊢ (↑(Int.negSucc a) : R) ∈ A 0

Tactic:
rw [Int.cast_negSucc]

Premises used: Int.cast_negSucc
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
a : ℕ
⊢ -(↑(a + 1) : R) ∈ A 0

Tactic:
neg_mem (SetLike.natCast_mem_graded _ _)

Premises used: SetLike.natCast_mem_graded, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
a : ℕ
⊢ -(↑(a + 1) : R) ∈ A 0

Tactic:
exact neg_mem (SetLike.natCast_mem_graded _ _)

Premises used: SetLike.natCast_mem_graded, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : AddMonoid ι
inst_5 : SetLike.GradedMonoid A
i : ι
x : ↥(A i)
⊢ (coeRingHom A : (a : ⨁ (i : ι), ↥(A i)) → R)
      (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
        ⨁ (i : ι), ↥(A i)) =
    (↑x : R)

Tactic:
DirectSum.toSemiring_of _ _ _ _ _

Premises used: DirectSum.toSemiring_of
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : AddMonoid ι
inst_5 : SetLike.GradedMonoid A
inst_6 : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
rw :
  Eq.{u_4 + 1} (α := R)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
      (↑(((((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (i.1 + i.2) : ↥(A (i.1 + i.2)) →+ ⨁ (i : ι), ↥(A i)) :
                    (a : ↥(A (i.1 + i.2))) → ⨁ (i : ι), ↥(A i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ i.1 i.2
                    ((r : (a : ι) → ↥(A a)) i.1 : ↥(A i.1)) ((r' : (a : ι) → ↥(A a)) i.2 : ↥(A i.2))) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    (∑ ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
      ij.1 + ij.2 = n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R))
⊢ (↑((r * r' : (a : ι) → ↥(A a)) n) : R) =
    ∑ ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
      ij.1 + ij.2 = n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R)

Tactic:
rw [mul_eq_sum_support_ghas_mul, DFinsupp.finsetSum_apply, AddSubmonoidClass.coe_finsetSum]

Premises used: DFinsupp.finsetSum_apply, AddSubmonoidClass.coe_finsetSum, DirectSum.mul_eq_sum_support_ghas_mul
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : AddMonoid ι
inst_5 : SetLike.GradedMonoid A
inst_6 : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
rw :
  (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (x : ι) (ai : ↥(A x)) ↦
                DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (x_1 : ι) (aj : ↥(A x_1)) ↦
                  ((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (x + x_1) : ↥(A (x + x_1)) →+ ⨁ (i : ι), ↥(A i)) :
                      (a : ↥(A (x + x_1))) → ⨁ (i : ι), ↥(A i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ai aj) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          n) :
      R) =
    DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i : ι) (ri : ↥(A i)) ↦
      DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
        if i + j = n then (↑ri : R) * (↑rj : R) else 0
⊢ (↑((r * r' : (a : ι) → ↥(A a)) n) : R) =
    DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i : ι) (ri : ↥(A i)) ↦
      DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
        if i + j = n then (↑ri : R) * (↑rj : R) else 0

Tactic:
rw [mul_eq_dfinsuppSum]

Premises used: DirectSum.mul_eq_dfinsuppSum
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : AddMonoid ι
inst_5 : SetLike.GradedMonoid A
inst_6 : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
rw :
  Eq (α := R)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r,
      (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (x : ι) (aj : ↥(A x)) ↦
                  ((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (i + x) : ↥(A (i + x)) →+ ⨁ (i : ι), ↥(A i)) :
                      (a : ↥(A (i + x))) → ⨁ (i : ι), ↥(A i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) i)
                      aj) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i : ι) (ri : ↥(A i)) ↦
      DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
        if i + j = n then (↑ri : R) * (↑rj : R) else 0)
⊢ (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (x : ι) (ai : ↥(A x)) ↦
                DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (x_1 : ι) (aj : ↥(A x_1)) ↦
                  ((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (x + x_1) : ↥(A (x + x_1)) →+ ⨁ (i : ι), ↥(A i)) :
                      (a : ↥(A (x + x_1))) → ⨁ (i : ι), ↥(A i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ai aj) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          n) :
      R) =
    DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i : ι) (ri : ↥(A i)) ↦
      DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
        if i + j = n then (↑ri : R) * (↑rj : R) else 0

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

Premises used: AddSubmonoidClass.coe_finsetSum, DFinsupp.sum, DFinsupp.sum_apply
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : AddMonoid ι
inst_5 : SetLike.GradedMonoid A
inst_6 : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
e_f :
  Eq (α := ι → R)
    (fun (i : ι) ↦
      (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (x : ι) (aj : ↥(A x)) ↦
                  ((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (i + x) : ↥(A (i + x)) →+ ⨁ (i : ι), ↥(A i)) :
                      (a : ↥(A (i + x))) → ⨁ (i : ι), ↥(A i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) i)
                      aj) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    fun (i : ι) ↦
    (fun (i : ι) (ri : ↥(A i)) ↦
        (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
            if i + j = n then (↑ri : R) * (↑rj : R) else 0 :
          R))
      i ((r : (a : ι) → ↥(A a)) i)
⊢ Eq (α := R)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r,
      (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (x : ι) (aj : ↥(A x)) ↦
                  ((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (i + x) : ↥(A (i + x)) →+ ⨁ (i : ι), ↥(A i)) :
                      (a : ↥(A (i + x))) → ⨁ (i : ι), ↥(A i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) i)
                      aj) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i : ι) (ri : ↥(A i)) ↦
      DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
        if i + j = n then (↑ri : R) * (↑rj : R) else 0)

Tactic:
congr
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : AddMonoid ι
inst_5 : SetLike.GradedMonoid A
inst_6 : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
e_f :
  ∀ (x : ι),
    (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (x_1 : ι) (aj : ↥(A x_1)) ↦
                  ((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (x + x_1) : ↥(A (x + x_1)) →+ ⨁ (i : ι), ↥(A i)) :
                      (a : ↥(A (x + x_1))) → ⨁ (i : ι), ↥(A i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) x)
                      aj) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R) =
      (fun (i : ι) (ri : ↥(A i)) ↦
          (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
              if i + j = n then (↑ri : R) * (↑rj : R) else 0 :
            R))
        x ((r : (a : ι) → ↥(A a)) x)
⊢ Eq (α := ι → R)
    (fun (i : ι) ↦
      (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (x : ι) (aj : ↥(A x)) ↦
                  ((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (i + x) : ↥(A (i + x)) →+ ⨁ (i : ι), ↥(A i)) :
                      (a : ↥(A (i + x))) → ⨁ (i : ι), ↥(A i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) i)
                      aj) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    fun (i : ι) ↦
    (fun (i : ι) (ri : ↥(A i)) ↦
        (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
            if i + j = n then (↑ri : R) * (↑rj : R) else 0 :
          R))
      i ((r : (a : ι) → ↥(A a)) i)

Tactic:
ext