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 _ _ _ _
Proof state after:
case a.refine'_1
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'

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'

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'

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'