internlm/Lean-Github huggingface dataset:
Theorem: rel_of_sum_of_rel_add
Proof state before:
case empty
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
⊢ (∀ i ∈ ∅, r (f i) (g i)) → r (∅.sum f) (∅.sum g)
Tactic:
exact fun _ =>  hr_zero
Proof state after:
no goals
Theorem: rel_of_sum_of_rel_add
Proof state before:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
⊢ (∀ i_1 ∈ insert i s, r (f i_1) (g i_1)) → r ((insert i s).sum f) ((insert i s).sum g)
Tactic:
intro H
Proof state after:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
H : ∀ i_1 ∈ insert i s, r (f i_1) (g i_1)
⊢ r ((insert i s).sum f) ((insert i s).sum g)
Theorem: rel_of_sum_of_rel_add
Proof state before:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
H : ∀ i_1 ∈ insert i s, r (f i_1) (g i_1)
⊢ r ((insert i s).sum f) ((insert i s).sum g)
Tactic:
simp only [Finset.sum_insert hi]
Proof state after:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
H : ∀ i_1 ∈ insert i s, r (f i_1) (g i_1)
⊢ r (f i + ∑ x ∈ s, f x) (g i + ∑ x ∈ s, g x)
Theorem: rel_of_sum_of_rel_add
Proof state before:
case insert
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
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r (f i) (g i)) → r (s.sum f) (s.sum g)
H : ∀ i_1 ∈ insert i s, r (f i_1) (g i_1)
⊢ r (f i + ∑ x ∈ s, f x) (g i + ∑ x ∈ s, g x)
Tactic:
exact hr_add (H _ (Finset.mem_insert_self _ _))
  (hs (fun _ hi => H _ (Finset.mem_insert_of_mem hi)))
Proof state after:
no goals
Theorem: rel_of_finsupp_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
H : ∀ (i : ι), r (f i) (g i)
⊢ r (f.sum fun x x => x) (g.sum fun x x => x)
Tactic:
rw [Finsupp.sum_of_support_subset f (Finset.subset_union_left _ g.support),
  Finsupp.sum_of_support_subset g (Finset.subset_union_right f.support _)]
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
H : ∀ (i : ι), r (f i) (g i)
⊢ r (∑ x ∈ f.support ∪ g.support, f x) (∑ x ∈ f.support ∪ g.support, g x)

case h
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
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

case h
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
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0
Theorem: rel_of_finsupp_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
H : ∀ (i : ι), r (f i) (g i)
⊢ r (∑ x ∈ f.support ∪ g.support, f x) (∑ x ∈ f.support ∪ g.support, g x)

case h
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
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

case h
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
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0
Tactic:
exact rel_of_sum_of_rel_add hr_zero hr_add (fun i _ =>  H i)
Proof state after:
case h
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
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

case h
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
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0
Theorem: rel_of_finsupp_sum_of_rel_add
Proof state before:
case h
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
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0

case h
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
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0
Tactic:
all_goals { intro _ _ ; rfl }
Proof state after:
no goals
Theorem: rel_of_finsupp_sum_of_rel_add
Proof state before:
case h
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
H : ∀ (i : ι), r (f i) (g i)
⊢ ∀ i ∈ f.support ∪ g.support, 0 = 0
Tactic:
intro _ _
Proof state after:
case h
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
H : ∀ (i : ι), r (f i) (g i)
i✝ : ι
a✝ : i✝ ∈ f.support ∪ g.support
⊢ 0 = 0
Theorem: rel_of_finsupp_sum_of_rel_add
Proof state before:
case h
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
H : ∀ (i : ι), r (f i) (g i)
i✝ : ι
a✝ : i✝ ∈ f.support ∪ g.support
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: rel_of_dsum_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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
s : Finset ι
H : ∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))
⊢ r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
s : Finset ι
⊢ (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
Theorem: rel_of_dsum_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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
s : Finset ι
⊢ (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
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
Theorem: rel_of_dsum_of_rel_add
Proof state before:
case empty
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
⊢ (∀ i ∈ ∅, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ ∅, (h i) (f i)) (∑ i ∈ ∅, (h i) (g i))
Tactic:
exact fun _ => hr_zero
Proof state after:
no goals
Theorem: rel_of_dsum_of_rel_add
Proof state before:
case insert
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
⊢ (∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))) →
    r (∑ i ∈ insert i s, (h i) (f i)) (∑ i ∈ insert i s, (h i) (g i))
Tactic:
intro H
Proof state after:
case insert
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
H : ∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))
⊢ r (∑ i ∈ insert i s, (h i) (f i)) (∑ i ∈ insert i s, (h i) (g i))
Theorem: rel_of_dsum_of_rel_add
Proof state before:
case insert
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
H : ∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))
⊢ r (∑ i ∈ insert i s, (h i) (f i)) (∑ i ∈ insert i s, (h i) (g i))
Tactic:
simp only [Finset.sum_insert hi]
Proof state after:
case insert
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
H : ∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))
⊢ r ((h i) (f i) + ∑ i ∈ s, (h i) (f i)) ((h i) (g i) + ∑ i ∈ s, (h i) (g i))
Theorem: rel_of_dsum_of_rel_add
Proof state before:
case insert
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 ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
f g : (i : ι) → β i
h : (i : ι) → β i →+ A
i : ι
s : Finset ι
hi : i ∉ s
hs : (∀ i ∈ s, r ((h i) (f i)) ((h i) (g i))) → r (∑ i ∈ s, (h i) (f i)) (∑ i ∈ s, (h i) (g i))
H : ∀ i_1 ∈ insert i s, r ((h i_1) (f i_1)) ((h i_1) (g i_1))
⊢ r ((h i) (f i) + ∑ i ∈ s, (h i) (f i)) ((h i) (g i) + ∑ i ∈ s, (h i) (g i))
Tactic:
exact hr_add (H _ (Finset.mem_insert_self _ _))
  (hs (fun _ hi => H _ (Finset.mem_insert_of_mem hi)))
Proof state after:
no goals
Theorem: rel_of_dfinsupp_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 ι
β : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (y : β i) → Decidable (y ≠ 0)
h h' : (i : ι) → β i →+ A
f g : DFinsupp β
H : ∀ (i : ι), r ((h i) (f i)) ((h' i) (g i))
⊢ r (f.sum fun i y => (h i) y) (g.sum fun i y => (h' i) y)
Tactic:
rw [DFinsupp.sum_of_support_le (Finset.subset_union_left f.support g.support),
  DFinsupp.sum_of_support_le (Finset.subset_union_right f.support g.support)]
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 ι
β : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (y : β i) → Decidable (y ≠ 0)
h h' : (i : ι) → β i →+ A
f g : DFinsupp β
H : ∀ (i : ι), r ((h i) (f i)) ((h' i) (g i))
⊢ r (∑ i ∈ f.support ∪ g.support, (h i) (f i)) (∑ i ∈ f.support ∪ g.support, (h' i) (g i))
Theorem: rel_of_dfinsupp_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 ι
β : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (y : β i) → Decidable (y ≠ 0)
h h' : (i : ι) → β i →+ A
f g : DFinsupp β
H : ∀ (i : ι), r ((h i) (f i)) ((h' i) (g i))
⊢ r (∑ i ∈ f.support ∪ g.support, (h i) (f i)) (∑ i ∈ f.support ∪ g.support, (h' i) (g i))
Tactic:
exact rel_of_sum_of_rel_add hr_zero hr_add (fun i _ => H i)
Proof state after:
no goals
Theorem: RingConGen.RelIsHomogeneous_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 𝒜 (Rel 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 : Rel rel a b
⊢ ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Theorem: RingConGen.RelIsHomogeneous_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 : Rel rel a b
⊢ ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
induction h with
| of x y h => exact fun i =>  RingConGen.Rel.of _ _ (hr h i)
| refl x => exact fun _ => RingConGen.Rel.refl _
| symm _ h' => exact fun i => RingConGen.Rel.symm (h' i)
| trans _ _ k k' => exact fun i => RingConGen.Rel.trans (k i) (k' i)
| add _ _  k k' =>
  intro i
  simp only [map_add]
  exact RingConGen.Rel.add (k i) (k' i)
| @mul a b c d _ _ k k' =>
  intro n
  simp only [AlgEquiv.toLinearMap_apply, map_mul, coe_mul_apply_eq_dfinsupp_sum]
  apply rel_of_dfinsupp_sum_of_rel_add (RingConGen.Rel.refl 0) (RingConGen.Rel.add)
    (Φy 𝒜 n (decomposeAlgEquiv 𝒜 c)) (Φy 𝒜 n (decomposeAlgEquiv 𝒜 d))
  intro i
  apply rel_of_dfinsupp_sum_of_rel_add (RingConGen.Rel.refl 0) (RingConGen.Rel.add)
  intro j
  dsimp only [Φ]
  by_cases hn : i + j = n
  . simp only [if_pos hn]
    exact RingConGen.Rel.mul (k i) (k' j)
  . simp only [if_neg hn]
    exact RingConGen.Rel.refl _
Proof state after:
no goals
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case of
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 x y : A
h : rel x y
⊢ ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap x) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap y) i)
Tactic:
exact fun i =>  RingConGen.Rel.of _ _ (hr h i)
Proof state after:
no goals
Theorem: RingConGen.RelIsHomogeneous_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 x : A
⊢ ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap x) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap x) i)
Tactic:
exact fun _ => RingConGen.Rel.refl _
Proof state after:
no goals