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 : 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
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₇ :
  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

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)

Premises used: LE.le.trans_eq, self_le_add_right, ite_self, MulZeroClass.zero_mul, DFinsupp.sum_zero, DFinsupp.sum, Finset.sum_const_zero, Finset.sum_ite_of_false, 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 : 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.{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

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 : 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
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
⊢ 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:
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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
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 : 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₁)) ↦ 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
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₁)) ↦ 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
h₁ : ∀ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r, ¬x + 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

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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ ∀ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r, ¬x + i = n

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

Premises used: LE.le.trans_eq, self_le_add_left, 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ ∀ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r, ¬x + i = n

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

Premises used: LE.le.trans_eq, self_le_add_left
-- 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
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
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₈ :
  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

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)

Premises used: LE.le.trans_eq, ite_self, DFinsupp.sum_zero, self_le_add_left, DFinsupp.sum, Finset.sum_const_zero, MulZeroClass.mul_zero, Finset.sum_ite_of_false, 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 : 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 : ι
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:
coe_mul_of_apply_aux _ _ _ fun _x => (eq_tsub_iff_add_eq_of_le h).symm

Premises used: Set.Mem, DirectSum.coe_mul_of_apply_aux, eq_tsub_iff_add_eq_of_le, Iff.symm
-- 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
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
rw₁ rw₂ : x + i = n ↔ x + i = n
⊢ i + x = n ↔ x = n - i

Tactic:
rw [eq_tsub_iff_add_eq_of_le h, add_comm]

Premises used: add_comm, eq_tsub_iff_add_eq_of_le
-- 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
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst_11 : Decidable (i ≤ n)
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)
neg :
  ∀ (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
⊢ (↑((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

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 : 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)
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:
coe_mul_of_apply_of_le _ _ _ n h

Premises used: DirectSum.coe_mul_of_apply_of_le
-- 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
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst_11 : Decidable (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

Tactic:
coe_mul_of_apply_of_not_le _ _ _ n h

Premises used: DirectSum.coe_mul_of_apply_of_not_le
-- 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
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst_11 : Decidable (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) =
    (↑((r : (a : ι) → ↥(A a)) (n - i)) : R) * (↑r' : R)

Tactic:
exacts [coe_mul_of_apply_of_le _ _ _ n h, coe_mul_of_apply_of_not_le _ _ _ n h]

Premises used: DirectSum.coe_mul_of_apply_of_le
-- 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
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst_11 : Decidable (i ≤ n)
pos :
  ∀ (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) =
      (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) (n - i)) : R)
neg :
  ∀ (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
⊢ (↑((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) =
    if i ≤ n then (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) (n - i)) : R) else 0

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 : 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 : ι
inst_11 : Decidable (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) =
    (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) (n - i)) : R)

Tactic:
coe_of_mul_apply_of_le _ _ _ n h

Premises used: DirectSum.coe_of_mul_apply_of_le
-- 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
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst_11 : Decidable (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

Tactic:
coe_of_mul_apply_of_not_le _ _ _ n h

Premises used: DirectSum.coe_of_mul_apply_of_not_le
-- 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
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst_11 : Decidable (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) =
    (↑r : R) * (↑((r' : (a : ι) → ↥(A a)) (n - i)) : R)

Tactic:
exacts [coe_of_mul_apply_of_le _ _ _ n h, coe_of_mul_apply_of_not_le _ _ _ n h]

Premises used: DirectSum.coe_of_mul_apply_of_le
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
S : Type u_3
R : Type u_4
ι : Type u_5
inst : AddMonoid ι
inst_1 : CommSemiring S
inst_2 : Semiring R
inst_3 : Algebra S R
A : ι → Submodule S R
inst_4 : SetLike.GradedMonoid A
s : S
⊢ Eq.{u_4 + 1} (α := R)
    ((↑(((@GAlgebra.toFun.{u_5, u_3, u_4} _ S (fun (i : ι) ↦ ↥(A i)) inst_1 (fun (i : ι) ↦ (A i).addCommMonoid)
                  (fun (i : ι) ↦ (A i).module) inst (SetLike.gsemiring A) _ :
                AddMonoidHom.{u_3, u_4} 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
σ : Type u_2
S : Type u_3
R : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring S
inst_2 : Semiring R
inst_3 : Algebra S R
p : Submodule S R
rw : 1 ≤ HPow.hPow (β := ℕ) p 0
rw₁ rw₂ : LE.le.{u_4} (α := Submodule S R) 1 1
⊢ 1 ∈ HPow.hPow (β := ℕ) p 0

Tactic:
rw [← one_le, pow_zero]

Premises used: pow_zero, Submodule.one_le
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring S
inst_2 : Semiring R
inst_3 : Algebra S R
p_1 : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p_1 ^ i
hq : q ∈ p_1 ^ j
rw : p * q ∈ p_1 ^ i * p_1 ^ j
⊢ p * q ∈ p_1 ^ (i + j)

Tactic:
rw [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring S
inst_2 : Semiring R
inst_3 : Algebra S R
p_1 : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p_1 ^ i
hq : q ∈ p_1 ^ j
⊢ p * q ∈ p_1 ^ i * p_1 ^ j

Tactic:
Submodule.mul_mem_mul hp hq

Premises used: Submodule.mul_mem_mul, Set.Mem
-- Module: Mathlib.Algebra.DirectSum.Internal
Goal:
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst : DecidableEq ι
inst_1 : CommSemiring S
inst_2 : Semiring R
inst_3 : Algebra S R
p_1 : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p_1 ^ i
hq : q ∈ p_1 ^ j
⊢ p * q ∈ p_1 ^ i * p_1 ^ j

Tactic:
exact Submodule.mul_mem_mul hp hq

Premises used: Submodule.mul_mem_mul
-- 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
⊢ Eq (α := Submodule S R) (⨆ (i : ι), A i : Submodule S R)
    ((Subalgebra.toSubmodule : (a : Subalgebra S R) → Submodule S R) (AlgHom.range (coeAlgHom A)) : Submodule S R)

Tactic:
(Submodule.iSup_eq_range_dfinsupp_lsum A).trans <| SetLike.coe_injective rfl

Premises used: Submodule.iSup_eq_range_dfinsupp_lsum, SetLike.coe_injective, rfl, Eq.trans
-- 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)
⊢ Eq.{u_4 + 1} (α := R)
    ((LinearMap.toAddMonoidHom.{u_3, u_3, u_4, u_4} (R := S) (S := S) (modM₁ := (fun (i : ι) ↦ (A i).module) 0)
            (modM₂ := Algebra.toModule) (σ := RingHom.id S) ((fun (i : ι) ↦ (A i).subtype) 0) :
          (a : (fun (i : ι) ↦ ↥(A i)) 0) → R)
        (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ (fun (i : ι) ↦ ↥(A i)) i) AddZero.toZero _ :
          (fun (i : ι) ↦ ↥(A i)) 0) :
      R)
    (1 : R)

Tactic:
rfl