awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
S : Type u_3
R : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring S
inst_3 : Semiring R
inst_4 : Algebra S R
A : ι → Submodule S R
inst_5 : SetLike.GradedMonoid A
i : ι
x : ↥(A i)
i_1 j : ι
x_1 : (fun (i : ι) ↦ ↥(A i)) i_1
x_2 : (fun (i : ι) ↦ ↥(A i)) j
⊢ (LinearMap.toAddMonoidHom.{u_3, u_3, u_4, u_4} (R := S) (S := S) (modM₁ := (fun (i : ι) ↦ (A i).module) (i_1 + j))
          (modM₂ := Algebra.toModule) (σ := RingHom.id S) ((fun (i : ι) ↦ (A i).subtype) (i_1 + j)) :
        (a : (fun (i : ι) ↦ ↥(A i)) (i_1 + j)) → R)
      (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ (fun (i : ι) ↦ ↥(A i)) i) AddSemigroup.toAdd _ _ _ x_1 x_2 :
        (fun (i : ι) ↦ ↥(A i)) (i_1 + j)) =
    HMul.hMul (α := R) (β := R)
      ((LinearMap.toAddMonoidHom.{u_3, u_3, u_4, u_4} (R := S) (S := S) (modM₁ := (fun (i : ι) ↦ (A i).module) i_1)
              (modM₂ := Algebra.toModule) (σ := RingHom.id S) ((fun (i : ι) ↦ (A i).subtype) i_1) :
            (a : (fun (i : ι) ↦ ↥(A i)) i_1) → R)
          x_1 :
        R)
      ((LinearMap.toAddMonoidHom.{u_3, u_3, u_4, u_4} (R := S) (S := S) (modM₁ := (fun (i : ι) ↦ (A i).module) j)
              (modM₂ := Algebra.toModule) (σ := RingHom.id S) ((fun (i : ι) ↦ (A i).subtype) j) :
            (a : (fun (i : ι) ↦ ↥(A i)) j) → R)
          x_2 :
        R)

Tactic:
rfl
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : AddMonoid ι
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedMonoid A
n : ℕ
⊢ Eq.{u_4 + 1} (α := R) (↑(↑n : ↥(A 0)) : R) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : AddMonoid ι
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedMonoid A
n : ℕ
inst_5 : n.AtLeastTwo
⊢ Eq.{u_4 + 1} (α := R) (↑(OfNat.ofNat n) : R) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : CommSemiring R
inst_1 : AddMonoid ι
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedMonoid A
x : ↥(A 0)
⊢ (algebraMap (↥(A 0)) R : (a : ↥(A 0)) → R) x = (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Ring R
inst_1 : AddMonoid ι
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedMonoid A
z : ℤ
⊢ Eq.{u_4 + 1} (α := R) (↑(↑z : ↥(A 0)) : R) (↑z : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
S : Type u_3
R : Type u_4
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : Algebra S R
inst_3 : AddMonoid ι
A : ι → Submodule S R
inst_4 : GradedMonoid A
s : S
⊢ Eq.{u_4 + 1} (α := R) ((↑((algebraMap S ↥(A 0) : (a : S) → ↥(A 0)) s) : R) : R) ((algebraMap S R : (a : S) → R) s : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
S : Type u_3
R : Type u_4
inst : Zero ι
inst_1 : Semiring S
inst_2 : AddCommMonoid R
inst_3 : Module S R
A : ι → Submodule S R
⊢ IsHomogeneousElem A 0

Tactic:
⟨0, Submodule.zero_mem _⟩

Premises used: Submodule.zero_mem, Exists.intro, OfNat.ofNat, SetLike.IsHomogeneousElem
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
S : Type u_3
R : Type u_4
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : Algebra S R
A : ι → Submodule S R
s : S
r : R
hr : IsHomogeneousElem A r
⊢ IsHomogeneousElem A (s • r)

Tactic:
let ⟨i, hi⟩ := hr
  ⟨i, Submodule.smul_mem _ _ hi⟩

Premises used: _private.0.SetLike.Homogeneous.smul.match_1, Exists.intro, HSMul.hSMul, SetLike.IsHomogeneousElem, Submodule.smul_mem
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
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 = k, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R))
    0
⊢ (r * r' : (a : ι) → ↥(A a)) k = 0

Tactic:
rw [Subtype.ext_iff, ZeroMemClass.coe_zero, coe_mul_apply]

Premises used: DirectSum.coe_mul_apply, Subtype.ext_iff, ZeroMemClass.coe_zero
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
apply :
  ∀ (x : ι × ι)
    (hx :
      x ∈
        {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
          ij.1 + ij.2 = k}),
    (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
⊢ 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 = k, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R))
    0

Tactic:
apply Finset.sum_eq_zero fun x hx ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
x : ι × ι
hx :
  x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = k}
by_contra! : ∀ (hm : m ≤ x.1) (hn : n ≤ x.2), False
⊢ x.1 < m ∨ x.2 < n

Tactic:
by_contra! ⟨hm, hn⟩
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
x : ι × ι
hx :
  x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = k}
hm : m ≤ x.1
hn : n ≤ x.2
⊢ x.1 + x.2 = k

Tactic:
simp_all
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
x : ι × ι
hx :
  x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = k}
hm : m ≤ x.1
hn : n ≤ x.2
⊢ x.1 + x.2 < m + n

Tactic:
obtain rfl : x.1 + x.2 = k := by simp_all

Premises used: Prod.fst, Prod.snd, rfl
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
x : ι × ι
hx :
  x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = k}
hm : m ≤ x.1
hn : n ≤ x.2
hk₁ : x.1 + x.2 < m + n
⊢ x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = x.1 + x.2}

Tactic:
obtain rfl : x.1 + x.2 = k := by simp_all

Premises used: Prod.fst, Prod.snd, rfl
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
x : ι × ι
hm : m ≤ x.1
hn : n ≤ x.2
hk : x.1 + x.2 < m + n
hx :
  x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = x.1 + x.2}
⊢ m + n ≤ x.1 + x.2

Tactic:
gcongr
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
x : ι × ι
hm : m ≤ x.1
hn : n ≤ x.2
hk : x.1 + x.2 < m + n
hx :
  x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = x.1 + x.2}
⊢ False

Tactic:
apply lt_irrefl (m + n) <| lt_of_le_of_lt (by gcongr) hk

Premises used: lt_of_le_of_lt, lt_irrefl, HAdd.hAdd
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
x : ι × ι
hx :
  x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = k}
inl : ∀ (hx : x.1 < m), (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
inr : ∀ (hx : x.2 < n), (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
⊢ (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0

Tactic:
obtain (hx | hx) : x.1 < m ∨ x.2 < n := by
    by_contra! ⟨hm, hn⟩
    obtain rfl : x.1 + x.2 = k := by simp_all
    apply lt_irrefl (m + n) <| lt_of_le_of_lt (by gcongr) hk

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
x : ι × ι
hx_1 :
  x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = k}
hx : x.1 < m
⊢ (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0

Tactic:
simp [hr, hr', hx]
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
x : ι × ι
hx_1 :
  x ∈
    {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
      ij.1 + ij.2 = k}
hx : x.2 < n
⊢ (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0

Tactic:
simp [hr, hr', hx]
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, (r : (a : ι) → ↥(A a)) i = 0
hr' : ∀ i < n, (r' : (a : ι) → ↥(A a)) i = 0
k : ι
hk : k < m + n
rw : (↑((r * r' : (a : ι) → ↥(A a)) k) : R) = (↑0 : R)
rw₁ : (↑((r * r' : (a : ι) → ↥(A a)) k) : R) = 0
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 = k, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R))
    0
rw₅ :
  ∀ (x : ι × ι)
    (hx :
      x ∈
        {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
          ij.1 + ij.2 = k}),
    (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
inl :
  ∀ (x : ι × ι)
    (hx :
      x ∈
        {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
          ij.1 + ij.2 = k})
    (hx : x.1 < m), (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
inr :
  ∀ (x : ι × ι)
    (hx :
      x ∈
        {ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' |
          ij.1 + ij.2 = k})
    (hx : x.2 < n), (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
⊢ (r * r' : (a : ι) → ↥(A a)) k = 0

Tactic:
classical
  rw [Subtype.ext_iff, ZeroMemClass.coe_zero, coe_mul_apply]
  apply Finset.sum_eq_zero fun x hx ↦ ?_
  obtain (hx | hx) : x.1 < m ∨ x.2 < n := by
    by_contra! ⟨hm, hn⟩
    obtain rfl : x.1 + x.2 = k := by simp_all
    apply lt_irrefl (m + n) <| lt_of_le_of_lt (by gcongr) hk
  all_goals simp [hr, hr', hx]

Premises used: Finset.sum_eq_zero, DirectSum.coe_mul_apply, Subtype.ext_iff, ZeroMemClass.coe_zero
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
hl :
  ∀ (xn : (⨁ (i : ι), ↥(A i)) × ι),
    Membership.mem (γ := List ((⨁ (i : ι), ↥(A i)) × ι)) [] xn → ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < List.sum (List.map (α := (⨁ (i : ι), ↥(A i)) × ι) Prod.snd [])
⊢ ((List.prod (List.map (α := (⨁ (i : ι), ↥(A i)) × ι) Prod.fst []) : ⨁ (i : ι), ↥(A i)) : (a : ι) → ↥(A a)) n = 0

Tactic:
simp at hn
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
head : (⨁ (i : ι), ↥(A i)) × ι
tail : List ((⨁ (i : ι), ↥(A i)) × ι)
ih :
  ∀ (hl : ∀ xn ∈ tail, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < (List.map Prod.snd tail).sum),
    ((List.map Prod.fst tail).prod : (a : ι) → ↥(A a)) n = 0
hl : ∀ xn ∈ head :: tail, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < (List.map Prod.snd (head :: tail)).sum
cons :
  ∀ (hl : (∀ k < head.2, (head.1 : (a : ι) → ↥(A a)) k = 0) ∧ ∀ a ∈ tail, ∀ k < a.2, (a.1 : (a : ι) → ↥(A a)) k = 0),
    (head.1 * (List.map Prod.fst tail).prod : (a : ι) → ↥(A a)) n = 0
⊢ ((List.map Prod.fst (head :: tail)).prod : (a : ι) → ↥(A a)) n = 0

Tactic:
simp only [List.mem_cons, forall_eq_or_imp, List.map_cons, List.sum_cons,
      List.prod_cons] at hl hn ⊢

Premises used: List.map_cons, forall_eq_or_imp, List.sum_cons, List.mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
head : (⨁ (i : ι), ↥(A i)) × ι
tail : List ((⨁ (i : ι), ↥(A i)) × ι)
ih :
  ∀ (hl : ∀ xn ∈ tail, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < (List.map Prod.snd tail).sum),
    ((List.map Prod.fst tail).prod : (a : ι) → ↥(A a)) n = 0
n : ι
hn : n < head.2 + (List.map Prod.snd tail).sum
hl : (∀ k < head.2, (head.1 : (a : ι) → ↥(A a)) k = 0) ∧ ∀ a ∈ tail, ∀ k < a.2, (a.1 : (a : ι) → ↥(A a)) k = 0
⊢ (head.1 * (List.map Prod.fst tail).prod : (a : ι) → ↥(A a)) n = 0

Tactic:
mul_apply_eq_zero hl.1 (ih hl.2) hn

Premises used: mul_apply_eq_zero, And.right, And.left
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
head : (⨁ (i : ι), ↥(A i)) × ι
tail : List ((⨁ (i : ι), ↥(A i)) × ι)
ih :
  ∀ (hl : ∀ xn ∈ tail, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < (List.map Prod.snd tail).sum),
    ((List.map Prod.fst tail).prod : (a : ι) → ↥(A a)) n = 0
n : ι
hn : n < head.2 + (List.map Prod.snd tail).sum
hl : (∀ k < head.2, (head.1 : (a : ι) → ↥(A a)) k = 0) ∧ ∀ a ∈ tail, ∀ k < a.2, (a.1 : (a : ι) → ↥(A a)) k = 0
⊢ (head.1 * (List.map Prod.fst tail).prod : (a : ι) → ↥(A a)) n = 0

Tactic:
exact mul_apply_eq_zero hl.1 (ih hl.2) hn

Premises used: mul_apply_eq_zero, And.right, And.left
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
l : List ((⨁ (i : ι), ↥(A i)) × ι)
hl : ∀ xn ∈ l, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < (List.map Prod.snd l).sum
nil :
  ∀
    (hl :
      ∀ (xn : (⨁ (i : ι), ↥(A i)) × ι),
        Membership.mem (γ := List ((⨁ (i : ι), ↥(A i)) × ι)) [] xn → ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0)
    ⦃n : ι⦄ (hn : n < List.sum (List.map (α := (⨁ (i : ι), ↥(A i)) × ι) Prod.snd [])),
    ((List.prod (List.map (α := (⨁ (i : ι), ↥(A i)) × ι) Prod.fst []) : ⨁ (i : ι), ↥(A i)) : (a : ι) → ↥(A a)) n = 0
cons :
  ∀ (head : (⨁ (i : ι), ↥(A i)) × ι) (tail : List ((⨁ (i : ι), ↥(A i)) × ι))
    (ih :
      ∀ (hl : ∀ xn ∈ tail, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < (List.map Prod.snd tail).sum),
        ((List.map Prod.fst tail).prod : (a : ι) → ↥(A a)) n = 0)
    (hl : ∀ xn ∈ head :: tail, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄
    (hn : n < (List.map Prod.snd (head :: tail)).sum),
    ((List.map Prod.fst (head :: tail)).prod : (a : ι) → ↥(A a)) n = 0
⊢ ((List.map Prod.fst l).prod : (a : ι) → ↥(A a)) n = 0

Tactic:
induction l generalizing n with
  | nil => simp at hn
  | cons head tail ih =>
    simp only [List.mem_cons, forall_eq_or_imp, List.map_cons, List.sum_cons,
      List.prod_cons] at hl hn ⊢
    exact mul_apply_eq_zero hl.1 (ih hl.2) hn

Premises used: List.map_cons, forall_eq_or_imp, List.sum_cons, List.mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
m : ι
hl :
  ∀ (x : ⨁ (i : ι), ↥(A i)), Membership.mem (γ := List (⨁ (i : ι), ↥(A i))) [] x → ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < List.length (α := ⨁ (i : ι), ↥(A i)) [] • m
⊢ ((List.prod [] : ⨁ (i : ι), ↥(A i)) : (a : ι) → ↥(A a)) n = 0

Tactic:
simp at hn
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih :
  ∀ (hl : ∀ x ∈ tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < tail.length • m),
    (tail.prod : (a : ι) → ↥(A a)) n = 0
hl : ∀ x ∈ head :: tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < (head :: tail).length • m
cons :
  ∀ (hl : (∀ k < m, (head : (a : ι) → ↥(A a)) k = 0) ∧ ∀ a ∈ tail, ∀ k < m, (a : (a : ι) → ↥(A a)) k = 0),
    (head * tail.prod : (a : ι) → ↥(A a)) n = 0
⊢ ((head :: tail).prod : (a : ι) → ↥(A a)) n = 0

Tactic:
simp only [List.mem_cons, forall_eq_or_imp, List.length_cons, List.prod_cons] at hl hn ⊢

Premises used: List.length_cons, forall_eq_or_imp, List.mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih :
  ∀ (hl : ∀ x ∈ tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < tail.length • m),
    (tail.prod : (a : ι) → ↥(A a)) n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, (head : (a : ι) → ↥(A a)) k = 0) ∧ ∀ a ∈ tail, ∀ k < m, (a : (a : ι) → ↥(A a)) k = 0
⊢ (head * tail.prod : (a : ι) → ↥(A a)) n = 0

Tactic:
mul_apply_eq_zero hl.1 (ih hl.2) ?_

Premises used: mul_apply_eq_zero, And.right, And.left
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih :
  ∀ (hl : ∀ x ∈ tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < tail.length • m),
    (tail.prod : (a : ι) → ↥(A a)) n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, (head : (a : ι) → ↥(A a)) k = 0) ∧ ∀ a ∈ tail, ∀ k < m, (a : (a : ι) → ↥(A a)) k = 0
cons : n < m + tail.length • m
⊢ (head * tail.prod : (a : ι) → ↥(A a)) n = 0

Tactic:
refine mul_apply_eq_zero hl.1 (ih hl.2) ?_

Premises used: mul_apply_eq_zero, And.right, And.left
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih :
  ∀ (hl : ∀ x ∈ tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < tail.length • m),
    (tail.prod : (a : ι) → ↥(A a)) n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, (head : (a : ι) → ↥(A a)) k = 0) ∧ ∀ a ∈ tail, ∀ k < m, (a : (a : ι) → ↥(A a)) k = 0
⊢ n < m + tail.length • m

Tactic:
simpa [add_smul, add_comm m] using hn

Premises used: add_comm, add_smul