internlm/Lean-Github huggingface dataset:
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case h.left
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx : x✝ ∈ Ideal.ofRel r
x a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ r' ↑((Decomposition.decompose' a) i) ↑((Decomposition.decompose' b) i)
Tactic:
use 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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx : x✝ ∈ Ideal.ofRel r
x a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ ↑((Decomposition.decompose' a) i) ∈ 𝒜 i ∧
    ↑((Decomposition.decompose' b) i) ∈ 𝒜 i ∧ r ↑((Decomposition.decompose' a) i) ↑((Decomposition.decompose' b) i)
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx : x✝ ∈ Ideal.ofRel r
x a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ ↑((Decomposition.decompose' a) i) ∈ 𝒜 i ∧
    ↑((Decomposition.decompose' b) i) ∈ 𝒜 i ∧ r ↑((Decomposition.decompose' a) i) ↑((Decomposition.decompose' b) i)
Tactic:
simp only [Decomposition.decompose'_eq, SetLike.coe_mem, true_and]
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx : x✝ ∈ Ideal.ofRel r
x a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ r ↑(((decompose fun i => 𝒜 i) a) i) ↑(((decompose fun i => 𝒜 i) b) i)
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx : x✝ ∈ Ideal.ofRel r
x a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ r ↑(((decompose fun i => 𝒜 i) a) i) ↑(((decompose fun i => 𝒜 i) b) i)
Tactic:
simp only [Rel.IsHomogeneous] at hr
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr :
  ∀ {a b : A},
    r a b → ∀ (i : ι), r ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx : x✝ ∈ Ideal.ofRel r
x a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ r ↑(((decompose fun i => 𝒜 i) a) i) ↑(((decompose fun i => 𝒜 i) b) i)
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr :
  ∀ {a b : A},
    r a b → ∀ (i : ι), r ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx : x✝ ∈ Ideal.ofRel r
x a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ r ↑(((decompose fun i => 𝒜 i) a) i) ↑(((decompose fun i => 𝒜 i) b) i)
Tactic:
exact hr h' i
Proof state after:
no goals
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case h.right
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx : x✝ ∈ Ideal.ofRel r
x a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ ↑((Decomposition.decompose' x) i) + ↑((Decomposition.decompose' b) i) = ↑((Decomposition.decompose' a) i)
Tactic:
simp only [← h, Decomposition.decompose'_eq, decompose_add,
  add_apply, AddSubmonoid.coe_add, Submodule.coe_toAddSubmonoid]
Proof state after:
no goals
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_2
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x : A
hx : x ∈ Ideal.ofRel r
⊢ 0 ∈ Ideal.ofRel r'
Tactic:
simp only [Submodule.zero_mem]
Proof state after:
no goals
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_3
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x : A
hx : x ∈ Ideal.ofRel r
⊢ ∀ (x y : A), x ∈ Ideal.ofRel r' → y ∈ Ideal.ofRel r' → x + y ∈ Ideal.ofRel r'
Tactic:
intro x y hx hy
Proof state after:
case a.refine'_3
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx✝ : x✝ ∈ Ideal.ofRel r
x y : A
hx : x ∈ Ideal.ofRel r'
hy : y ∈ Ideal.ofRel r'
⊢ x + y ∈ Ideal.ofRel r'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_3
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx✝ : x✝ ∈ Ideal.ofRel r
x y : A
hx : x ∈ Ideal.ofRel r'
hy : y ∈ Ideal.ofRel r'
⊢ x + y ∈ Ideal.ofRel r'
Tactic:
exact Ideal.add_mem _ hx hy
Proof state after:
no goals
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_4
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x : A
hx : x ∈ Ideal.ofRel r
⊢ ∀ (a x : A), x ∈ Ideal.ofRel r' → a • x ∈ Ideal.ofRel r'
Tactic:
intro a x hx
Proof state after:
case a.refine'_4
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx✝ : x✝ ∈ Ideal.ofRel r
a x : A
hx : x ∈ Ideal.ofRel r'
⊢ a • x ∈ Ideal.ofRel r'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_4
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx✝ : x✝ ∈ Ideal.ofRel r
a x : A
hx : x ∈ Ideal.ofRel r'
⊢ a • x ∈ Ideal.ofRel r'
Tactic:
simp only [smul_eq_mul]
Proof state after:
case a.refine'_4
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx✝ : x✝ ∈ Ideal.ofRel r
a x : A
hx : x ∈ Ideal.ofRel r'
⊢ a * x ∈ Ideal.ofRel r'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_4
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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx✝ : x✝ ∈ Ideal.ofRel r
a x : A
hx : x ∈ Ideal.ofRel r'
⊢ a * x ∈ Ideal.ofRel r'
Tactic:
apply Ideal.mul_mem_left _ _ hx
Proof state after:
no goals
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case 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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
⊢ Ideal.ofRel r' ≤ Ideal.ofRel r
Tactic:
intro x hx'
Proof state after:
case 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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x : A
hx' : x ∈ Ideal.ofRel r'
⊢ x ∈ Ideal.ofRel r
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case 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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x : A
hx' : x ∈ Ideal.ofRel r'
⊢ x ∈ Ideal.ofRel r
Tactic:
refine' Submodule.span_induction hx' _ (Submodule.zero_mem _)
  (fun _ _ hx hy => Ideal.add_mem _ hx hy) (fun a _ hx => Ideal.mul_mem_left _ a hx)
Proof state after:
case 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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x : A
hx' : x ∈ Ideal.ofRel r'
⊢ ∀ x ∈ {x | ∃ a b, r' a b ∧ x + b = a}, x ∈ Ideal.ofRel r
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case 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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x : A
hx' : x ∈ Ideal.ofRel r'
⊢ ∀ x ∈ {x | ∃ a b, r' a b ∧ x + b = a}, x ∈ Ideal.ofRel r
Tactic:
. rintro x ⟨a, b, ⟨i, _, _, h'⟩, h⟩
  exact Ideal.subset_span  ⟨a, b, h', h⟩
Proof state after:
no goals
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case 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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x : A
hx' : x ∈ Ideal.ofRel r'
⊢ ∀ x ∈ {x | ∃ a b, r' a b ∧ x + b = a}, x ∈ Ideal.ofRel r
Tactic:
rintro x ⟨a, b, ⟨i, _, _, h'⟩, h⟩
Proof state after:
case a.intro.intro.intro.intro.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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx' : x✝ ∈ Ideal.ofRel r'
x a b : A
h : x + b = a
i : ι
left✝¹ : a ∈ 𝒜 i
left✝ : b ∈ 𝒜 i
h' : r a b
⊢ x ∈ Ideal.ofRel r
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.intro.intro.intro.intro.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
R : Type u_4
inst✝⁵ : CommRing R
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_6
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
r : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 r
r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
x✝ : A
hx' : x✝ ∈ Ideal.ofRel r'
x a b : A
h : x + b = a
i : ι
left✝¹ : a ∈ 𝒜 i
left✝ : b ∈ 𝒜 i
h' : r a b
⊢ x ∈ Ideal.ofRel r
Tactic:
exact Ideal.subset_span  ⟨a, b, h', h⟩
Proof state after:
no goals
Theorem: foo_mul
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
h𝒜 : GradedAlgebra 𝒜
a b : RingQuot rel
i j : ι
ha : a ∈ quotSubmodule R 𝒜 rel i
hb : b ∈ quotSubmodule R 𝒜 rel j
⊢ a * b ∈ quotSubmodule R 𝒜 rel (i + j)
Tactic:
obtain ⟨a, ha, rfl⟩ := ha
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
h𝒜 : GradedAlgebra 𝒜
b : RingQuot rel
i j : ι
hb : b ∈ quotSubmodule R 𝒜 rel j
a : A
ha : a ∈ ↑(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) a * b ∈ quotSubmodule R 𝒜 rel (i + j)
Theorem: foo_mul
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
h𝒜 : GradedAlgebra 𝒜
b : RingQuot rel
i j : ι
hb : b ∈ quotSubmodule R 𝒜 rel j
a : A
ha : a ∈ ↑(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) a * b ∈ quotSubmodule R 𝒜 rel (i + j)
Tactic:
obtain ⟨b, hb, rfl⟩ := hb
Proof state after:
case intro.intro.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
h𝒜 : GradedAlgebra 𝒜
i j : ι
a : A
ha : a ∈ ↑(𝒜 i)
b : A
hb : b ∈ ↑(𝒜 j)
⊢ (RingQuot.mkAlgHom R rel) a * (RingQuot.mkAlgHom R rel) b ∈ quotSubmodule R 𝒜 rel (i + j)
Theorem: foo_mul
Proof state before:
case intro.intro.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
h𝒜 : GradedAlgebra 𝒜
i j : ι
a : A
ha : a ∈ ↑(𝒜 i)
b : A
hb : b ∈ ↑(𝒜 j)
⊢ (RingQuot.mkAlgHom R rel) a * (RingQuot.mkAlgHom R rel) b ∈ quotSubmodule R 𝒜 rel (i + j)
Tactic:
rw [← map_mul]
Proof state after:
case intro.intro.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
h𝒜 : GradedAlgebra 𝒜
i j : ι
a : A
ha : a ∈ ↑(𝒜 i)
b : A
hb : b ∈ ↑(𝒜 j)
⊢ (RingQuot.mkAlgHom R rel) (a * b) ∈ quotSubmodule R 𝒜 rel (i + j)
Theorem: foo_mul
Proof state before:
case intro.intro.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
h𝒜 : GradedAlgebra 𝒜
i j : ι
a : A
ha : a ∈ ↑(𝒜 i)
b : A
hb : b ∈ ↑(𝒜 j)
⊢ (RingQuot.mkAlgHom R rel) (a * b) ∈ quotSubmodule R 𝒜 rel (i + j)
Tactic:
exact ⟨a * b, h𝒜.mul_mem ha hb, rfl⟩
Proof state after:
no goals
Theorem: quotDecompose_left_inv'_aux
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
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel) =
    (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜
Tactic:
apply linearMap_ext
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
⊢ ∀ (i : ι),
    ((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ
        lof R ι (fun i => ↥(𝒜 i)) i =
      ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i