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
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)
neg : ∀ (h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'), 0 = (↑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)

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
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'
⊢ (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R) = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : 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
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
neg₂ neg₃ : Eq.{u_4 + 1} (α := R) 0 0
⊢ 0 = (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)

Tactic:
rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]

Premises used: DFinsupp.notMem_support_iff, MulZeroClass.mul_zero, ZeroMemClass.coe_zero, Iff.mp
-- 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 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)
neg neg₁ :
  ∀ (h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r'), 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:
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]

Premises used: Finset.sum_ite_eq', ite_self, MulZeroClass.zero_mul, DFinsupp.sum_zero, DFinsupp.sum, MulZeroClass.mul_zero, ZeroMemClass.coe_zero, DirectSum.coe_mul_apply_eq_dfinsuppSum, 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = 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₂ : ι) (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)
⊢ (↑((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)

Tactic:
rw [coe_mul_apply_eq_dfinsuppSum, DFinsupp.sum_comm]

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

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

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

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

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

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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : j ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r
⊢ (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R) = (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r
neg : 0 = (↑0 : R) * (↑r' : R)
neg₁ : 0 = 0 * (↑r' : R)
neg₂ neg₃ : Eq.{u_4 + 1} (α := R) 0 0
⊢ 0 = (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)

Tactic:
rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]

Premises used: DFinsupp.notMem_support_iff, MulZeroClass.zero_mul, ZeroMemClass.coe_zero, Iff.mp
-- 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
rw :
  (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i_1 : ι) (ri : ↥(A i_1)) ↦
      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 (j : ι) (rj : ↥(A j)) ↦ if i_1 + j = n then (↑ri : R) * (↑rj : R) else 0) =
    (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
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₂ : ι) (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)
rw₄ :
  (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦
      if i₁ + i = n then (↑x₁ : R) * (↑r' : R) else 0) =
    (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
rw₅ rw₆ :
  Eq (α := R)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦
      if i₁ + i = n then (↑x₁ : R) * (↑0 : R) else 0)
    0
rw₇ rw₈ :
  (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦
      if i₁ + i = n then (↑x₁ : R) * (↑r' : R) else 0) =
    (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
rw₉ :
  (if j ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r then (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R) else 0) =
    (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
pos :
  ∀ (h : j ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r),
    (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R) = (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
neg neg₁ : ∀ (h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r), 0 = (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
⊢ (↑((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)

Tactic:
classical
    rw [coe_mul_apply_eq_dfinsuppSum, DFinsupp.sum_comm]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, mul_zero, 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, zero_mul]

Premises used: Finset.sum_ite_eq', ite_self, MulZeroClass.zero_mul, DFinsupp.sum_zero, DFinsupp.sum, MulZeroClass.mul_zero, ZeroMemClass.coe_zero, DFinsupp.sum_comm, DirectSum.coe_mul_apply_eq_dfinsuppSum, 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 : AddLeftCancelMonoid ι
inst_5 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
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))
          (i + j)) :
      R) =
    (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) j) : R)

Tactic:
coe_of_mul_apply_aux _ _ _ fun _x => ⟨fun h => add_left_cancel h, fun h => h ▸ rfl⟩

Premises used: DirectSum.coe_of_mul_apply_aux, Eq.rec, add_left_cancel, Iff.intro, 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 : AddRightCancelMonoid ι
inst_5 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
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))
          (j + i)) :
      R) =
    (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)

Tactic:
coe_mul_of_apply_aux _ _ _ fun _x => ⟨fun h => add_right_cancel h, fun h => h ▸ rfl⟩

Premises used: Eq.rec, add_right_cancel, DirectSum.coe_mul_of_apply_aux, Iff.intro, 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
r : ↥(A 0)
r' : ⨁ (i : ι), ↥(A i)
j _x : ι
rw rw₁ : _x = j ↔ _x = j
⊢ 0 + _x = j ↔ _x = j

Tactic:
rw [zero_add]

Premises used: zero_add
-- 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
r : ⨁ (i : ι), ↥(A i)
r' : ↥(A 0)
j _x : ι
rw rw₁ : _x = j ↔ _x = j
⊢ _x + 0 = j ↔ _x = j

Tactic:
rw [add_zero]

Premises used: add_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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
rw :
  Eq.{u_4 + 1} (α := 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)
    0
⊢ (↑((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) =
    0

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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
apply :
  Eq (α := R)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
      if i + j = n then (↑r : R) * (↑rj : R) else 0)
    0
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
⊢ Eq.{u_4 + 1} (α := 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)
    0

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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
h₁ : ∀ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r', ¬i + x = n
⊢ Eq (α := R)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r' fun (j : ι) (rj : ↥(A j)) ↦
      if i + j = n then (↑r : R) * (↑rj : R) else 0)
    0

Tactic:
rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]

Premises used: DFinsupp.sum, Finset.sum_const_zero, Finset.sum_ite_of_false
-- 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ ∀ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r', ¬i + x = n

Tactic:
fun x _ H => h ((self_le_add_right i x).trans_eq H)

Premises used: LE.le.trans_eq, self_le_add_right, Not
-- 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ ∀ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r', ¬i + x = n

Tactic:
exact fun x _ H => h ((self_le_add_right i x).trans_eq H)

Premises used: LE.le.trans_eq, self_le_add_right