awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 x : ι
e_f :
  Eq.{u_4 + 1} (α := R)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
      (↑(((((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (x + i) : ↥(A (x + i)) →+ ⨁ (i : ι), ↥(A i)) :
                    (a : ↥(A (x + i))) → ⨁ (i : ι), ↥(A i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) x)
                    ((r' : (a : ι) → ↥(A a)) i)) :
                ⨁ (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))
⊢ (↑(((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)

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 x : ι
e_f :
  Eq (α := ι → R)
    (fun (i : ι) ↦
      (↑(((((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (x + i) : ↥(A (x + i)) →+ ⨁ (i : ι), ↥(A i)) :
                    (a : ↥(A (x + i))) → ⨁ (i : ι), ↥(A i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) x)
                    ((r' : (a : ι) → ↥(A a)) i)) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    fun (i : ι) ↦
    (fun (j : ι) (rj : ↥(A j)) ↦ if x + j = n then (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑rj : R) else 0) i
      ((r' : (a : ι) → ↥(A a)) i)
⊢ Eq.{u_4 + 1} (α := R)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
      (↑(((((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (x + i) : ↥(A (x + i)) →+ ⨁ (i : ι), ↥(A i)) :
                    (a : ↥(A (x + i))) → ⨁ (i : ι), ↥(A i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) x)
                    ((r' : (a : ι) → ↥(A a)) i)) :
                ⨁ (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))

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 x : ι
e_f :
  ∀ (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)
                    ((r' : (a : ι) → ↥(A a)) x_1)) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R) =
      (fun (j : ι) (rj : ↥(A j)) ↦ if x + j = n then (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑rj : R) else 0) x_1
        ((r' : (a : ι) → ↥(A a)) x_1)
⊢ Eq (α := ι → R)
    (fun (i : ι) ↦
      (↑(((((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (x + i) : ↥(A (x + i)) →+ ⨁ (i : ι), ↥(A i)) :
                    (a : ↥(A (x + i))) → ⨁ (i : ι), ↥(A i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) x)
                    ((r' : (a : ι) → ↥(A a)) i)) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    fun (i : ι) ↦
    (fun (j : ι) (rj : ↥(A j)) ↦ if x + j = n then (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑rj : R) else 0) i
      ((r' : (a : ι) → ↥(A a)) i)

Tactic:
ext
-- 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 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)
                    ((r' : (a : ι) → ↥(A a)) x_1)) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R) =
      (fun (j : ι) (rj : ↥(A j)) ↦ if x + j = n then (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑rj : R) else 0) x_1
        ((r' : (a : ι) → ↥(A a)) x_1)
⊢ (↑(((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:
iterate 2 rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]; congr; ext

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 x x_1 : ι
e_f :
  (↑(((((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)
                  ((r' : (a : ι) → ↥(A a)) x_1)) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          n) :
      R) =
    if x + x_1 = n then (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑((r' : (a : ι) → ↥(A a)) x_1) : R) else 0
⊢ (↑(((((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)
                  ((r' : (a : ι) → ↥(A a)) x_1)) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          n) :
      R) =
    (fun (j : ι) (rj : ↥(A j)) ↦ if x + j = n then (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑rj : R) else 0) x_1
      ((r' : (a : ι) → ↥(A a)) x_1)

Tactic:
dsimp only
-- 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 x x_1 : ι
pos :
  ∀ (h : x + x_1 = n),
    (↑(((((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)
                    ((r' : (a : ι) → ↥(A a)) x_1)) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R) =
      (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑((r' : (a : ι) → ↥(A a)) x_1) : R)
neg :
  ∀ (h : ¬x + x_1 = n),
    (↑(((((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)
                    ((r' : (a : ι) → ↥(A a)) x_1)) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R) =
      0
⊢ (↑(((((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)
                  ((r' : (a : ι) → ↥(A a)) x_1)) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          n) :
      R) =
    if x + x_1 = n then (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑((r' : (a : ι) → ↥(A a)) x_1) : R) else 0

Tactic:
split_ifs with h
-- 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 x x_1 : ι
h : x + x_1 = n
pos :
  (↑(((((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)
                  ((r' : (a : ι) → ↥(A a)) x_1)) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          (x + x_1)) :
      R) =
    (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑((r' : (a : ι) → ↥(A a)) x_1) : R)
⊢ (↑(((((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)
                  ((r' : (a : ι) → ↥(A a)) x_1)) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          n) :
      R) =
    (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑((r' : (a : ι) → ↥(A a)) x_1) : R)

Tactic:
subst h
-- 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)
x x_1 : ι
pos :
  (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) x)
            ((r' : (a : ι) → ↥(A a)) x_1) :
          ↥(A (x + x_1))) :
      R) =
    (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑((r' : (a : ι) → ↥(A a)) x_1) : R)
⊢ (↑(((((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)
                  ((r' : (a : ι) → ↥(A a)) x_1)) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          (x + x_1)) :
      R) =
    (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑((r' : (a : ι) → ↥(A a)) x_1) : R)

Tactic:
rw [of_eq_same]

Premises used: DirectSum.of_eq_same
-- 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)
x x_1 : ι
⊢ (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ _ ((r : (a : ι) → ↥(A a)) x)
            ((r' : (a : ι) → ↥(A a)) x_1) :
          ↥(A (x + x_1))) :
      R) =
    (↑((r : (a : ι) → ↥(A a)) x) : R) * (↑((r' : (a : ι) → ↥(A a)) x_1) : R)

Tactic:
rfl
-- 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 x x_1 : ι
h : ¬x + x_1 = n
neg : Eq.{u_4 + 1} (α := R) (↑0 : R) 0
⊢ (↑(((((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)
                  ((r' : (a : ι) → ↥(A a)) x_1)) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          n) :
      R) =
    0

Tactic:
rw [of_eq_of_ne _ _ _ (Ne.symm h)]

Premises used: Ne.symm, DirectSum.of_eq_of_ne
-- 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 x x_1 : ι
h : ¬x + x_1 = n
⊢ Eq.{u_4 + 1} (α := R) (↑0 : R) 0

Tactic:
rfl
-- 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 : HasAntidiagonal ι
inst_6 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
rw :
  Eq.{u_4 + 1} (α := 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))
    (∑ ij ∈ @antidiagonal _ inst_4 _ n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R))
⊢ (↑((r * r' : (a : ι) → ↥(A a)) n) : R) =
    ∑ ij ∈ @antidiagonal _ inst_4 _ n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R)

Tactic:
rw [coe_mul_apply]

Premises used: DirectSum.coe_mul_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 : HasAntidiagonal ι
inst_6 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
x : ι × ι
⊢ x ∈
      {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
        ij.1 + ij.2 = n} →
    x ∈ @antidiagonal _ inst_4 _ n

Tactic:
simp
-- 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 : HasAntidiagonal ι
inst_6 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
apply :
  ∀ x ∈ @antidiagonal _ inst_4 _ n,
    x ∉
        {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
          ij.1 + ij.2 = n} →
      (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
⊢ Eq.{u_4 + 1} (α := 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))
    (∑ ij ∈ @antidiagonal _ inst_4 _ n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R))

Tactic:
apply Finset.sum_subset (fun _ ↦ by simp)

Premises used: Finset.sum_subset
-- 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 : HasAntidiagonal ι
inst_6 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ∀ x ∈ @antidiagonal _ inst_4 _ n,
    x ∉
        {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
          ij.1 + ij.2 = n} →
      (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0

Tactic:
aesop (erase simp not_and) (add simp not_and_or)

Premises used: not_and_or, not_and
-- 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 : HasAntidiagonal ι
inst_6 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
rw rw₁ rw₂ :
  Eq.{u_4 + 1} (α := 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))
    (∑ ij ∈ @antidiagonal _ inst_4 _ n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R))
rw₃ :
  ∀ x ∈ @antidiagonal _ inst_4 _ n,
    x ∉
        {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
          ij.1 + ij.2 = n} →
      (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
⊢ (↑((r * r' : (a : ι) → ↥(A a)) n) : R) =
    ∑ ij ∈ @antidiagonal _ inst_4 _ n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R)

Tactic:
classical
  rw [coe_mul_apply]
  apply Finset.sum_subset (fun _ ↦ by simp)
  aesop (erase simp not_and) (add simp not_and_or)

Premises used: DirectSum.coe_mul_apply, Finset.sum_subset, not_and_or, not_and
-- 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 : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
rw :
  (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i))
      (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (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) * (↑((r' : (a : ι) → ↥(A a)) j) : R)
⊢ (↑((HMul.hMul (α := ⨁ (i : ι), ↥(A i))
              (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) :
                    (a : ↥(A i)) → ⨁ (i : ι), ↥(A i))
                  r :
                ⨁ (i : ι), ↥(A i))
              r' :
            (a : ι) → ↥(A a))
          n) :
      R) =
    (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)

Tactic:
rw [coe_mul_apply_eq_dfinsuppSum]

Premises used: DirectSum.coe_mul_apply_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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
apply :
  (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
      if i + j = n then (↑r : R) * (↑rj : R) else 0) =
    (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)
apply₁ :
  Eq (α := R)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
      if i + j = n then (↑0 : R) * (↑rj : R) else 0)
    0
⊢ (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i))
      (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (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) * (↑((r' : (a : ι) → ↥(A a)) j) : R)

Tactic:
apply (DFinsupp.sum_single_index _).trans

Premises used: DFinsupp.sum_single_index, Eq.trans
-- 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 : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
simp_rw : Eq (α := R) (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦ 0) 0
⊢ Eq (α := R)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
      if i + j = n then (↑0 : R) * (↑rj : R) else 0)
    0

Tactic:
simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]

Premises used: ite_self, MulZeroClass.zero_mul, ZeroMemClass.coe_zero
-- 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 : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ Eq (α := R) (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦ 0) 0

Tactic:
DFinsupp.sum_zero

Premises used: DFinsupp.sum_zero
-- 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 : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ Eq (α := R) (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦ 0) 0

Tactic:
exact DFinsupp.sum_zero

Premises used: DFinsupp.sum_zero
-- 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 : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
simp_rw :
  (if j ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' then (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R) else 0) =
    (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)
⊢ (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
      if i + j = n then (↑r : R) * (↑rj : R) else 0) =
    (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)

Tactic:
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']

Premises used: Finset.sum_ite_eq', DFinsupp.sum