Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
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'
Tactic:
. rintro x ⟨a, b, h', h⟩
  rw [← h𝒜.left_inv x, ← sum_support_of _ (Decomposition.decompose' x),
    map_sum]
  apply Ideal.sum_mem
  intro i _
  rw [coeAddMonoidHom_of]
  apply Ideal.subset_span
  use h𝒜.decompose' a i
  use h𝒜.decompose' b i
  simp only [exists_prop]
  constructor
  . use i
    simp only [Decomposition.decompose'_eq, SetLike.coe_mem, true_and]
    simp only [Rel.IsHomogeneous] at hr
    exact hr h' i
  . simp only [← h, Decomposition.decompose'_eq, decompose_add,
      add_apply, AddSubmonoid.coe_add, Submodule.coe_toAddSubmonoid]
Proof state after:
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'