internlm/Lean-Github huggingface dataset:
Theorem: DirectSum.mk_eq_sum
Proof state before:
case neg
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∉ s
⊢ 0 = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Tactic:
rw [DFinsupp.finset_sum_apply, Finset.sum_eq_zero
  (fun j hj => of_eq_of_ne _ _ _ _ (ne_of_mem_of_not_mem hj hi))]
Proof state after:
no goals
Theorem: DirectSum.toAddMonoid_mk
Proof state before:
ι : Type u_1
inst✝³ : DecidableEq ι
R : Type u_2
inst✝² : Semiring R
β : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u_4
inst✝ : AddCommMonoid γ
ψ : (i : ι) → β i →+ γ
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
⊢ (toAddMonoid ψ) ((mk β s) x) = ∑ i ∈ s, (ψ i) (if h : i ∈ s then x ⟨i, h⟩ else 0)
Tactic:
rw [mk_eq_sum, map_sum, Finset.sum_congr rfl (fun i _ => toAddMonoid_of _ _ _)]
Proof state after:
no goals
Theorem: DirectSum.map_apply'
Proof state before:
ι : Type u_1
inst✝⁶ : DecidableEq ι
R : Type u_2
inst✝⁵ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝⁴ : (i : ι) → AddCommMonoid (β i)
inst✝³ : (i : ι) → AddCommMonoid (γ i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ (map h) x = (mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)
Tactic:
conv_lhs => rw [← sum_support_of β x]
Proof state after:
ι : Type u_1
inst✝⁶ : DecidableEq ι
R : Type u_2
inst✝⁵ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝⁴ : (i : ι) → AddCommMonoid (β i)
inst✝³ : (i : ι) → AddCommMonoid (γ i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ (map h) (∑ i ∈ DFinsupp.support x, (of β i) (x i)) = (mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)
Theorem: DirectSum.map_apply'
Proof state before:
ι : Type u_1
inst✝⁶ : DecidableEq ι
R : Type u_2
inst✝⁵ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝⁴ : (i : ι) → AddCommMonoid (β i)
inst✝³ : (i : ι) → AddCommMonoid (γ i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ (map h) (∑ i ∈ DFinsupp.support x, (of β i) (x i)) = (mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)
Tactic:
simp_rw [map_sum, map_of]
Proof state after:
ι : Type u_1
inst✝⁶ : DecidableEq ι
R : Type u_2
inst✝⁵ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝⁴ : (i : ι) → AddCommMonoid (β i)
inst✝³ : (i : ι) → AddCommMonoid (γ i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ ∑ x_1 ∈ DFinsupp.support x, (of (fun i => γ i) x_1) ((h x_1) (x x_1)) =
    (mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)
Theorem: DirectSum.map_apply'
Proof state before:
ι : Type u_1
inst✝⁶ : DecidableEq ι
R : Type u_2
inst✝⁵ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝⁴ : (i : ι) → AddCommMonoid (β i)
inst✝³ : (i : ι) → AddCommMonoid (γ i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ ∑ x_1 ∈ DFinsupp.support x, (of (fun i => γ i) x_1) ((h x_1) (x x_1)) =
    (mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)
Tactic:
rw [eq_comm]
Proof state after:
ι : Type u_1
inst✝⁶ : DecidableEq ι
R : Type u_2
inst✝⁵ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝⁴ : (i : ι) → AddCommMonoid (β i)
inst✝³ : (i : ι) → AddCommMonoid (γ i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ ((mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)) =
    ∑ x_1 ∈ DFinsupp.support x, (of (fun i => γ i) x_1) ((h x_1) (x x_1))
Theorem: DirectSum.map_apply'
Proof state before:
ι : Type u_1
inst✝⁶ : DecidableEq ι
R : Type u_2
inst✝⁵ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝⁴ : (i : ι) → AddCommMonoid (β i)
inst✝³ : (i : ι) → AddCommMonoid (γ i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ ((mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)) =
    ∑ x_1 ∈ DFinsupp.support x, (of (fun i => γ i) x_1) ((h x_1) (x x_1))
Tactic:
convert mk_eq_sum x.support fun i => (h i) (x i)
Proof state after:
case h.e'_3.a.h.e'_6
ι : Type u_1
inst✝⁶ : DecidableEq ι
R : Type u_2
inst✝⁵ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝⁴ : (i : ι) → AddCommMonoid (β i)
inst✝³ : (i : ι) → AddCommMonoid (γ i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
x✝ : ι
a✝ : x✝ ∈ DFinsupp.support x
⊢ (h x✝) (x x✝) = if h_1 : x✝ ∈ DFinsupp.support x then (h ↑⟨x✝, h_1⟩) (x ↑⟨x✝, h_1⟩) else 0
Theorem: DirectSum.map_apply'
Proof state before:
case h.e'_3.a.h.e'_6
ι : Type u_1
inst✝⁶ : DecidableEq ι
R : Type u_2
inst✝⁵ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝⁴ : (i : ι) → AddCommMonoid (β i)
inst✝³ : (i : ι) → AddCommMonoid (γ i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
x✝ : ι
a✝ : x✝ ∈ DFinsupp.support x
⊢ (h x✝) (x x✝) = if h_1 : x✝ ∈ DFinsupp.support x then (h ↑⟨x✝, h_1⟩) (x ↑⟨x✝, h_1⟩) else 0
Tactic:
rwa [dif_pos]
Proof state after:
no goals
Theorem: DirectSum.decomposeAlgEquiv_coe
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 𝒜
a : A
⊢ (decomposeAlgEquiv 𝒜) a = (decompose 𝒜) a
Tactic:
rfl
Proof state after:
no goals
Theorem: Rel.IsHomogeneous_of_isPureHomogeneous
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
⊢ IsHomogeneous 𝒜 rel
Tactic:
intro a b h i
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i : ι
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Theorem: Rel.IsHomogeneous_of_isPureHomogeneous
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i : ι
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
obtain ⟨j, ha, hb⟩ := hrel h
Proof state after:
case intro.intro
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Theorem: Rel.IsHomogeneous_of_isPureHomogeneous
Proof state before:
case intro.intro
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
by_cases hij : j = i
Proof state after:
case pos
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)

case neg
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Theorem: Rel.IsHomogeneous_of_isPureHomogeneous
Proof state before:
case pos
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)

case neg
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
. rw [← hij]
  simp only [AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_coe, decompose_of_mem_same, ha, hb, h]
Proof state after:
case neg
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Theorem: Rel.IsHomogeneous_of_isPureHomogeneous
Proof state before:
case neg
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
. simp only [AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_coe, decompose_of_mem_ne _ ha hij,
    decompose_of_mem_ne _ hb hij]
  exact hrel0
Proof state after:
no goals
Theorem: Rel.IsHomogeneous_of_isPureHomogeneous
Proof state before:
case pos
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
rw [← hij]
Proof state after:
case pos
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) j) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) j)
Theorem: Rel.IsHomogeneous_of_isPureHomogeneous
Proof state before:
case pos
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) j) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) j)
Tactic:
simp only [AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_coe, decompose_of_mem_same, ha, hb, h]
Proof state after:
no goals
Theorem: Rel.IsHomogeneous_of_isPureHomogeneous
Proof state before:
case neg
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
simp only [AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_coe, decompose_of_mem_ne _ ha hij,
  decompose_of_mem_ne _ hb hij]
Proof state after:
case neg
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel 0 0
Theorem: Rel.IsHomogeneous_of_isPureHomogeneous
Proof state before:
case neg
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 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel 0 0
Tactic:
exact hrel0
Proof state after:
no goals
Theorem: RingConGen.Rel.sum
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
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
s : Finset ι
hs : ∀ i ∈ s, r (a i) (b i)
⊢ RingConGen.Rel (⇑r) (s.sum a) (s.sum b)
Tactic:
revert 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
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
s : Finset ι
⊢ (∀ i ∈ s, r (a i) (b i)) → RingConGen.Rel (⇑r) (s.sum a) (s.sum b)
Theorem: RingConGen.Rel.sum
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
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
s : Finset ι
⊢ (∀ i ∈ s, r (a i) (b i)) → RingConGen.Rel (⇑r) (s.sum a) (s.sum b)
Tactic:
induction' s using Finset.induction_on with j t hj ht hjt
Proof state after:
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
⊢ (∀ i ∈ ∅, r (a i) (b i)) → RingConGen.Rel (⇑r) (∅.sum a) (∅.sum b)

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
α : 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)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)
Theorem: RingConGen.Rel.sum
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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
⊢ (∀ i ∈ ∅, r (a i) (b i)) → RingConGen.Rel (⇑r) (∅.sum a) (∅.sum b)

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
α : 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)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)
Tactic:
. exact fun _ =>  RingConGen.Rel.refl _
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
α : 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)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)
Theorem: RingConGen.Rel.sum
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
α : 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)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)
Tactic:
. intro hs
  simp only [Finset.sum_insert hj]
  apply RingConGen.Rel.add
  . exact RingConGen.Rel.of _ _ (hs j (Finset.mem_insert_self j t))
  . 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 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
α : Type u_4
inst✝¹ : Ring α
r : RingCon α
ι : Type u_5
inst✝ : DecidableEq ι
a b : ι → α
⊢ (∀ i ∈ ∅, r (a i) (b i)) → RingConGen.Rel (⇑r) (∅.sum a) (∅.sum b)
Tactic:
exact fun _ =>  RingConGen.Rel.refl _
Proof state after:
no goals
Theorem: RingConGen.Rel.sum
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
α : 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)
⊢ (∀ i ∈ insert j t, r (a i) (b i)) → RingConGen.Rel (⇑r) ((insert j t).sum a) ((insert j t).sum b)
Tactic:
intro hs
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
α : 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) ((insert j t).sum a) ((insert j t).sum b)
Theorem: RingConGen.Rel.sum
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
α : 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) ((insert j t).sum a) ((insert j t).sum b)
Tactic:
simp only [Finset.sum_insert hj]
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
α : 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 + ∑ x ∈ t, a x) (b j + ∑ x ∈ t, b x)
Theorem: RingConGen.Rel.sum
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
α : 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 + ∑ x ∈ t, a x) (b j + ∑ x ∈ t, b x)
Tactic:
apply RingConGen.Rel.add
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) (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)