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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (↑((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
have 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
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 : 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.{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
have 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
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 : 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
⊢ 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
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 : 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)) ↦
      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 : 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)) ↦
      if i + j = n then (↑r : R) * (↑rj : R) else 0)
    0
have h₁ : ∀ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r', ¬i + x = n
Tactic: rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (↑((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
have 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
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
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_right i x).trans_eq 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 : 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 rw₁ 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
have rw₃ : 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: 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
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_right i x).trans_eq 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 : 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 rw₁ 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
rw₃ :
  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
⊢ (↑((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
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
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_right i x).trans_eq 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (↑((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) =
    0
have 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₂ : ι) (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)
  0
Tactic: rw [coe_mul_apply_eq_dfinsuppSum, DFinsupp.sum_comm]
-- 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ 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₂ : ι) (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)
    0
have apply : Eq (α := R)
  (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦
    if i₁ + i = n then (↑x₁ : R) * (↑r' : 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
apply :
  Eq (α := R)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦
      if i₁ + i = n then (↑x₁ : R) * (↑r' : 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₂ : ι) (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)
    0
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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ Eq (α := R)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦
      if i₁ + i = n then (↑x₁ : R) * (↑r' : R) else 0)
    0
have h₁ : ∀ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r, ¬x + i = n
Tactic: rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (↑((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) =
    0
have rw : Eq (α := R)
  (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)
  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
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_left i x).trans_eq 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
rw :
  Eq (α := R)
    (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)
    0
⊢ (↑((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) =
    0
have 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₂ : ι) (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)
  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
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_left i x).trans_eq 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
rw :
  Eq (α := R)
    (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)
    0
rw₁ rw₂ 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₂ : ι) (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)
    0
⊢ (↑((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) =
    0
have rw₄ : Eq (α := R)
  (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦
    if i₁ + i = n then (↑x₁ : R) * (↑r' : 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
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_left i x).trans_eq 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
rw :
  Eq (α := R)
    (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)
    0
rw₁ rw₂ 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₂ : ι) (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)
    0
rw₄ :
  Eq (α := R)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) r fun (i₁ : ι) (x₁ : ↥(A i₁)) ↦
      if i₁ + i = n then (↑x₁ : R) * (↑r' : R) else 0)
    0
⊢ (↑((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) =
    0
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
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_left i x).trans_eq 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : i ≤ n
x : ι
⊢ i + x = n ↔ x = n - i
have rw : i + x = n ↔ x + i = n
Tactic: rw [eq_tsub_iff_add_eq_of_le h, add_comm]
-- 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : i ≤ n
x : ι
rw : i + x = n ↔ x + i = n
⊢ i + x = n ↔ x = n - i
have rw₁ : x + i = n ↔ x + i = n
Tactic: rw [eq_tsub_iff_add_eq_of_le h, add_comm]
-- 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 : AddCommMonoid ι
inst_5 : PartialOrder ι
inst_6 : CanonicallyOrderedAdd ι
inst_7 : SetLike.GradedMonoid A
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst_11 : Decidable (i ≤ n)
⊢ (↑((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) =
    if i ≤ n then (↑((r : (a : ι) → ↥(A a)) (n - i)) : R) * (↑r' : R) else 0
have pos : ∀ (h : i ≤ n),
  (↑((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)) (n - i)) : R) * (↑r' : R)
Tactic: split_ifs with h