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 : HasAntidiagonal ι
inst_6 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ 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))
have 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
Tactic: apply Finset.sum_subset (fun _ ↦ by simp)
-- 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: classical
  rw [coe_mul_apply]
  apply Finset.sum_subset (fun _ ↦ by simp)
  aesop (erase simp not_and) (add simp not_and_or)
-- 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 : ι
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))
⊢ (↑((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₃ : ∀ 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: classical
  rw [coe_mul_apply]
  apply Finset.sum_subset (fun _ ↦ by simp)
  aesop (erase simp not_and) (add simp not_and_or)
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (↑((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)
have 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)
Tactic: rw [coe_mul_apply_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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (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)
have 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)
Tactic: apply (DFinsupp.sum_single_index _).trans
-- 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
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)
⊢ (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)
have 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
Tactic: apply (DFinsupp.sum_single_index _).trans
-- 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
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)) ↦
      if i + j = n then (↑0 : R) * (↑rj : R) else 0)
    0
have simp_rw : Eq (α := R) (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦ 0) 0
Tactic: simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (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)
have 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)
Tactic: simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (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)
have pos : ∀ (h : j ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'),
  (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R) = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
pos :
  ∀ (h : j ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'),
    (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R) = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)
⊢ (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)
have neg : ∀ (h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'), 0 = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'
⊢ 0 = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)
have neg : 0 = (↑r : R) * (↑0 : R)
Tactic: rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'
neg : 0 = (↑r : R) * (↑0 : R)
⊢ 0 = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)
have neg₁ : 0 = (↑r : R) * 0
Tactic: rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'
neg : 0 = (↑r : R) * (↑0 : R)
neg₁ : 0 = (↑r : R) * 0
⊢ 0 = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)
have neg₂ : Eq.{u_4 + 1} (α := R) 0 0
Tactic: rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (↑((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)
have 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)
Tactic: classical
    rw [coe_mul_apply_eq_dfinsuppSum]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero
    simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
    split_ifs with h
    · rfl
    rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
rw rw₁ 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)
have rw₃ : (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: classical
    rw [coe_mul_apply_eq_dfinsuppSum]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero
    simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
    split_ifs with h
    · rfl
    rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
rw rw₁ 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)
rw₃ :
  (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)
⊢ (↑((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)
have rw₄ : 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: classical
    rw [coe_mul_apply_eq_dfinsuppSum]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero
    simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
    split_ifs with h
    · rfl
    rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
rw rw₁ 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)
rw₃ :
  (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)
rw₄ rw₅ :
  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
rw₆ rw₇ :
  (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)
⊢ (↑((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)
have 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)
Tactic: classical
    rw [coe_mul_apply_eq_dfinsuppSum]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero
    simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
    split_ifs with h
    · rfl
    rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
rw rw₁ 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)
rw₃ :
  (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)
rw₄ rw₅ :
  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
rw₆ rw₇ :
  (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)
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)
⊢ (↑((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)
have pos : ∀ (h : j ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'),
  (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R) = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)
Tactic: classical
    rw [coe_mul_apply_eq_dfinsuppSum]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero
    simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
    split_ifs with h
    · rfl
    rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
-- 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
rw rw₁ 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)
rw₃ :
  (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)
rw₄ rw₅ :
  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
rw₆ rw₇ :
  (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)
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)
pos :
  ∀ (h : j ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'),
    (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R) = (↑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)
have neg : ∀ (h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'), 0 = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)
Tactic: classical
    rw [coe_mul_apply_eq_dfinsuppSum]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero
    simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
    split_ifs with h
    · rfl
    rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
-- 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (↑((HMul.hMul (β := ⨁ (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))
                  r' :
                ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          n) :
      R) =
    (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
have 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₂ : ι) (x₂ : ↥(A i₂)) ↦
    DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦
      if i₁ + i₂ = n then (↑x₁ : R) * (↑x₂ : R) else 0) =
  (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
Tactic: rw [coe_mul_apply_eq_dfinsuppSum, DFinsupp.sum_comm]