awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
simp_rw simp_rw₁ :
  Eq.{u_4 + 1} (α := R)
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
      (↑(((((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (x.1 + x.2) : ↥(A (x.1 + x.2)) →+ ⨁ (i : ι), ↥(A i)) :
                    (a : ↥(A (x.1 + x.2))) → ⨁ (i : ι), ↥(A i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ x.1 x.2
                    ((r : (a : ι) → ↥(A a)) x.1 : ↥(A x.1)) ((r' : (a : ι) → ↥(A a)) x.2 : ↥(A x.2))) :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            n) :
        R))
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
      x.1 + x.2 = n, (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R))
⊢ 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))
have simp_rw₂ : Eq.{u_4 + 1} (α := R)
  (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
    (↑(if x.1 + x.2 = n then
            @GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ x.1 x.2
              ((r : (a : ι) → ↥(A a)) x.1 : ↥(A x.1)) ((r' : (a : ι) → ↥(A a)) x.2 : ↥(A x.2))
          else 0 :
          ↥(A (x.1 + x.2))) :
      R))
  (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
    x.1 + x.2 = n, (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R))
Tactic: simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ (↑((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
have 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
Tactic: rw [mul_eq_dfinsuppSum]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ (↑(((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
have 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)
Tactic: rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ 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)
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ (↑(((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)
have 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))
Tactic: rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ (↑(((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
have 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)
Tactic: iterate 2 rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]; congr; ext
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ (↑(((((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
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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)
⊢ (↑(((((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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ (↑(((((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)
have 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)
Tactic: subst h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ (↑(((((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)
have 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)
Tactic: rw [of_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ (↑(((((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
have neg : Eq.{u_4 + 1} (α := R) (↑0 : R) 0
Tactic: rw [of_eq_of_ne _ _ _ (Ne.symm h)]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 : ι
⊢ (↑((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)
have 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))
Tactic: rw [coe_mul_apply]