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
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)
⊢ (↑((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 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
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 : 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)
⊢ (↑((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
have 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)
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 : 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)
⊢ (↑((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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ 1 ∈ HPow.hPow (β := ℕ) p 0
have rw : 1 ≤ HPow.hPow (β := ℕ) p 0
Tactic: rw [← one_le, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ 1 ∈ HPow.hPow (β := ℕ) p 0
have rw₁ : LE.le.{u_4} (α := Submodule S R) 1 1
Tactic: rw [← one_le, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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 + j)
have rw : p * q ∈ p_1 ^ i * p_1 ^ j
Tactic: rw [pow_add]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ (r * r' : (a : ι) → ↥(A a)) k = 0
have 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
Tactic: rw [Subtype.ext_iff, ZeroMemClass.coe_zero, coe_mul_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ 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
have 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
Tactic: apply Finset.sum_eq_zero fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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}
⊢ x.1 < m ∨ x.2 < n
have by_contra! : ∀ (hm : m ≤ x.1) (hn : n ≤ x.2), False
Tactic: by_contra! ⟨hm, hn⟩
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (hypothesis)
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
⊢ False
have hk₁ : x.1 + x.2 < m + n
Tactic: obtain rfl : x.1 + x.2 = k := by simp_all
Cleared hypotheses: k, hk, hx
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (hypothesis)
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
⊢ False
have 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}
Tactic: obtain rfl : x.1 + x.2 = k := by simp_all
Cleared hypotheses: k, hk, hx
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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}
⊢ (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
have inl : ∀ (hx : x.1 < m), (↑((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
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ (↑((r : (a : ι) → ↥(A a)) x.1) : R) * (↑((r' : (a : ι) → ↥(A a)) x.2) : R) = 0
have inr : ∀ (hx : x.2 < n), (↑((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
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ (r * r' : (a : ι) → ↥(A a)) k = 0
have rw : (↑((r * r' : (a : ι) → ↥(A a)) k) : R) = (↑0 : R)
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]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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)
⊢ (r * r' : (a : ι) → ↥(A a)) k = 0
have rw₁ : (↑((r * r' : (a : ι) → ↥(A a)) k) : R) = 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]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ (r * r' : (a : ι) → ↥(A a)) k = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ (r * r' : (a : ι) → ↥(A a)) k = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ (r * r' : (a : ι) → ↥(A a)) k = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ (r * r' : (a : ι) → ↥(A a)) k = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ ((List.map Prod.fst (head :: tail)).prod : (a : ι) → ↥(A a)) n = 0
have 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
Tactic: simp only [List.mem_cons, forall_eq_or_imp, List.map_cons, List.sum_cons,
      List.prod_cons] at hl hn ⊢
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ ((List.map Prod.fst l).prod : (a : ι) → ↥(A a)) n = 0
have 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
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
Cleared hypotheses: l, hl, n, hn
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
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
⊢ ((List.map Prod.fst l).prod : (a : ι) → ↥(A a)) n = 0
have 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
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
Cleared hypotheses: l, hl, n, hn