internlm/Lean-Github huggingface dataset:
Theorem: RingConGen.Rel.sum
Proof state before:
case insert.a
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (a j) (b j)

case insert.a
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (∑ x ∈ t, a x) (∑ x ∈ t, b x)
Tactic:
. exact RingConGen.Rel.of _ _ (hs j (Finset.mem_insert_self j t))
Proof state after:
case insert.a
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (∑ x ∈ t, a x) (∑ x ∈ t, b x)
Theorem: RingConGen.Rel.sum
Proof state before:
case insert.a
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (∑ x ∈ t, a x) (∑ x ∈ t, b x)
Tactic:
. exact ht (fun i hi =>  hs i (Finset.mem_insert_of_mem hi))
Proof state after:
no goals
Theorem: RingConGen.Rel.sum
Proof state before:
case insert.a
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (a j) (b j)
Tactic:
exact RingConGen.Rel.of _ _ (hs j (Finset.mem_insert_self j t))
Proof state after:
no goals
Theorem: RingConGen.Rel.sum
Proof state before:
case insert.a
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
j : ι
t : Finset ι
hj : j ∉ t
ht : (∀ i ∈ t, r (a i) (b i)) → RingConGen.Rel (⇑r) (t.sum a) (t.sum b)
hs : ∀ i ∈ insert j t, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (∑ x ∈ t, a x) (∑ x ∈ t, b x)
Tactic:
exact ht (fun i hi =>  hs i (Finset.mem_insert_of_mem hi))
Proof state after:
no goals
Theorem: DFinsupp.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ (x.sum fun i y => (h i) y) = ∑ i ∈ s, (h i) (x i)
Tactic:
simp only [DFinsupp.sum]
Proof state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∑ x_1 ∈ x.support, (h x_1) (x x_1) = ∑ x_1 ∈ s, (h x_1) (x x_1)
Theorem: DFinsupp.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∑ x_1 ∈ x.support, (h x_1) (x x_1) = ∑ x_1 ∈ s, (h x_1) (x x_1)
Tactic:
apply Finset.sum_subset hs
Proof state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ x.support → (h x_1) (x x_1) = 0
Theorem: DFinsupp.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ x.support → (h x_1) (x x_1) = 0
Tactic:
. intro i _ hi'
  simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'
  rw [hi', map_zero]
Proof state after:
no goals
Theorem: DFinsupp.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ x.support → (h x_1) (x x_1) = 0
Tactic:
intro i _ hi'
Proof state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
i : ι
a✝ : i ∈ s
hi' : i ∉ x.support
⊢ (h i) (x i) = 0
Theorem: DFinsupp.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
i : ι
a✝ : i ∈ s
hi' : i ∉ x.support
⊢ (h i) (x i) = 0
Tactic:
simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'
Proof state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
i : ι
a✝ : i ∈ s
hi' : x i = 0
⊢ (h i) (x i) = 0
Theorem: DFinsupp.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : DecidableEq A
inst✝² : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
i : ι
a✝ : i ∈ s
hi' : x i = 0
⊢ (h i) (x i) = 0
Tactic:
rw [hi', map_zero]
Proof state after:
no goals
Theorem: DirectSum.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ s, (of β i) (x i) = x
Tactic:
conv_rhs => rw [← sum_support_of β x]
Proof state after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ s, (of β i) (x i) = ∑ i ∈ DFinsupp.support x, (of β i) (x i)
Theorem: DirectSum.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ s, (of β i) (x i) = ∑ i ∈ DFinsupp.support x, (of β i) (x i)
Tactic:
rw [eq_comm]
Proof state after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ DFinsupp.support x, (of β i) (x i) = ∑ i ∈ s, (of β i) (x i)
Theorem: DirectSum.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ DFinsupp.support x, (of β i) (x i) = ∑ i ∈ s, (of β i) (x i)
Tactic:
apply Finset.sum_subset hs
Proof state after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ DFinsupp.support x → (of β x_1) (x x_1) = 0
Theorem: DirectSum.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ DFinsupp.support x → (of β x_1) (x x_1) = 0
Tactic:
. intro i _ hi'
  simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'
  rw [hi', map_zero]
Proof state after:
no goals
Theorem: DirectSum.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ DFinsupp.support x → (of β x_1) (x x_1) = 0
Tactic:
intro i _ hi'
Proof state after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
i : ι
a✝ : i ∈ s
hi' : i ∉ DFinsupp.support x
⊢ (of β i) (x i) = 0
Theorem: DirectSum.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
i : ι
a✝ : i ∈ s
hi' : i ∉ DFinsupp.support x
⊢ (of β i) (x i) = 0
Tactic:
simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'
Proof state after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
i : ι
a✝ : i ∈ s
hi' : x i = 0
⊢ (of β i) (x i) = 0
Theorem: DirectSum.sum_of_support_le
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
i : ι
a✝ : i ∈ s
hi' : x i = 0
⊢ (of β i) (x i) = 0
Tactic:
rw [hi', map_zero]
Proof state after:
no goals
Theorem: DirectSum.finsupp_sum_support_decompose'
Proof state before:
R : Type u_1
inst✝¹⁰ : CommSemiring R
ι✝ : Type u_2
inst✝⁹ : DecidableEq ι✝
inst✝⁸ : AddCommMonoid ι✝
A : Type u_3
inst✝⁷ : CommSemiring A
inst✝⁶ : DecidableEq A
inst✝⁵ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_3
M : Type u_1
σ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
inst : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ r = DFinsupp.sum ((decompose ℳ) r) fun i x => ↑x
Tactic:
conv_lhs => rw [← sum_support_decompose ℳ r]
Proof state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
ι✝ : Type u_2
inst✝⁹ : DecidableEq ι✝
inst✝⁸ : AddCommMonoid ι✝
A : Type u_3
inst✝⁷ : CommSemiring A
inst✝⁶ : DecidableEq A
inst✝⁵ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_3
M : Type u_1
σ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
inst : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) = DFinsupp.sum ((decompose ℳ) r) fun i x => ↑x
Theorem: DirectSum.finsupp_sum_support_decompose'
Proof state before:
R : Type u_1
inst✝¹⁰ : CommSemiring R
ι✝ : Type u_2
inst✝⁹ : DecidableEq ι✝
inst✝⁸ : AddCommMonoid ι✝
A : Type u_3
inst✝⁷ : CommSemiring A
inst✝⁶ : DecidableEq A
inst✝⁵ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_3
M : Type u_1
σ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
inst : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) = DFinsupp.sum ((decompose ℳ) r) fun i x => ↑x
Tactic:
rfl
Proof state after:
no goals
Theorem: EqvGenIsHomogeneous_of
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
⊢ Rel.IsHomogeneous 𝒜 (EqvGen rel)
Tactic:
intro a b h
Proof state after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a b : A
h : EqvGen rel a b
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Theorem: EqvGenIsHomogeneous_of
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a b : A
h : EqvGen rel a b
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
induction h with
| rel a b h => exact fun i => EqvGen.rel _ _ (hr h i)
| refl a => exact fun i => EqvGen.refl _
| symm a b _ k => exact fun i => EqvGen.symm _ _ (k i)
| trans a b c _ _ k k' => exact fun i => EqvGen.trans _ _ _ (k i) (k' i)
Proof state after:
no goals
Theorem: EqvGenIsHomogeneous_of
Proof state before:
case rel
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝ b✝ a b : A
h : rel a b
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
exact fun i => EqvGen.rel _ _ (hr h i)
Proof state after:
no goals
Theorem: EqvGenIsHomogeneous_of
Proof state before:
case refl
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝ b a : A
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i)
Tactic:
exact fun i => EqvGen.refl _
Proof state after:
no goals
Theorem: EqvGenIsHomogeneous_of
Proof state before:
case symm
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝¹ b✝ a b : A
a✝ : EqvGen rel a b
k : ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i)
Tactic:
exact fun i => EqvGen.symm _ _ (k i)
Proof state after:
no goals
Theorem: EqvGenIsHomogeneous_of
Proof state before:
case trans
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c : A
a✝¹ : EqvGen rel a b
a✝ : EqvGen rel b c
k : ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i)
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i)
Tactic:
exact fun i => EqvGen.trans _ _ _ (k i) (k' i)
Proof state after:
no goals
Theorem: rel_of_sum_of_rel_add
Proof state before:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A✝ : Type u_3
inst✝⁴ : CommSemiring A✝
inst✝³ : DecidableEq A✝
inst✝² : Algebra R A✝
𝒜 : ι✝ → Submodule R A✝
rel : A✝ → A✝ → Prop
A : Type u_4
inst✝¹ : AddCommMonoid A
r : A → A → Prop
hr_zero : r 0 0
hr_add : ∀ {a b c d : A}, r a c → r b d → r (a + b) (c + d)
ι : Type u_5
inst✝ : DecidableEq ι
f g : ι → A
s : Finset ι
H : ∀ i ∈ s, r (f i) (g i)
⊢ r (s.sum f) (s.sum g)
Tactic:
revert H
Proof state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A✝ : Type u_3
inst✝⁴ : CommSemiring A✝
inst✝³ : DecidableEq A✝
inst✝² : Algebra R A✝
𝒜 : ι✝ → Submodule R A✝
rel : A✝ → A✝ → Prop
A : Type u_4
inst✝¹ : AddCommMonoid A
r : A → A → Prop
hr_zero : r 0 0
hr_add : ∀ {a b c d : A}, r a c → r b d → r (a + b) (c + d)
ι : Type u_5
inst✝ : DecidableEq ι
f g : ι → A
s : Finset ι
⊢ (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
Theorem: rel_of_sum_of_rel_add
Proof state before:
R : Type u_1
inst✝⁷ : CommSemiring R
ι✝ : Type u_2
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : AddCommMonoid ι✝
A✝ : Type u_3
inst✝⁴ : CommSemiring A✝
inst✝³ : DecidableEq A✝
inst✝² : Algebra R A✝
𝒜 : ι✝ → Submodule R A✝
rel : A✝ → A✝ → Prop
A : Type u_4
inst✝¹ : AddCommMonoid A
r : A → A → Prop
hr_zero : r 0 0
hr_add : ∀ {a b c d : A}, r a c → r b d → r (a + b) (c + d)
ι : Type u_5
inst✝ : DecidableEq ι
f g : ι → A
s : Finset ι
⊢ (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
Tactic:
induction s using Finset.induction_on with
| empty => exact fun _ =>  hr_zero
| @insert i s hi hs =>
  intro H
  simp only [Finset.sum_insert hi]
  exact hr_add (H _ (Finset.mem_insert_self _ _))
    (hs (fun _ hi => H _ (Finset.mem_insert_of_mem hi)))
Proof state after:
no goals