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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = 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₂ : ι) (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)
have 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)
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
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)
⊢ (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)
have 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
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
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₁)) ↦
      if i₁ + i = n then (↑x₁ : R) * (↑0 : R) else 0)
    0
have simp_rw : Eq (α := R) (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦ 0) 0
Tactic: simp_rw [ZeroMemClass.coe_zero, mul_zero, 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (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)
have 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)
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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (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)
have 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)
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
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)
⊢ (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)
have neg : ∀ (h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r), 0 = (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : 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
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
⊢ 0 = (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
have neg : 0 = (↑0 : R) * (↑r' : R)
Tactic: rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
-- 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
h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r
neg : 0 = (↑0 : R) * (↑r' : R)
⊢ 0 = (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
have neg₁ : 0 = 0 * (↑r' : R)
Tactic: rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
-- 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
h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r
neg : 0 = (↑0 : R) * (↑r' : R)
neg₁ : 0 = 0 * (↑r' : R)
⊢ 0 = (↑((r : (a : ι) → ↥(A a)) j) : R) * (↑r' : R)
have neg₂ : Eq.{u_4 + 1} (α := R) 0 0
Tactic: rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
-- 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)) 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)
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]
-- 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
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)
⊢ (↑((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: 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]
-- 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
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)
⊢ (↑((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)) 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: 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]
-- 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
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)
⊢ (↑((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₅ : 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: 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]
-- 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
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)
⊢ (↑((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₉ : (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: 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]
-- 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
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)
⊢ (↑((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 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)
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]
-- 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
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)
⊢ (↑((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 neg : ∀ (h : j ∉ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r), 0 = (↑((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]
-- 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 : ↥(A 0)
r' : ⨁ (i : ι), ↥(A i)
j _x : ι
⊢ 0 + _x = j ↔ _x = j
have rw : _x = j ↔ _x = j
Tactic: rw [zero_add]
-- 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)
r' : ↥(A 0)
j _x : ι
⊢ _x + 0 = j ↔ _x = j
have rw : _x = j ↔ _x = j
Tactic: rw [add_zero]