internlm/Lean-Github huggingface dataset:
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'

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 x y hx hy
  exact Ideal.add_mem _ hx hy
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), 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), x ∈ Ideal.ofRel r' → a • x ∈ Ideal.ofRel r'
Tactic:
. intro a x hx
  simp only [smul_eq_mul]
  apply Ideal.mul_mem_left _ _ hx
Proof state after:
no goals
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'
Tactic:
rintro x ⟨a, b, h', h⟩
Proof state after:
case a.refine'_1.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' : r a b
h : x + b = a
⊢ x ∈ Ideal.ofRel r'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_1.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' : r a b
h : x + b = a
⊢ x ∈ Ideal.ofRel r'
Tactic:
rw [← h𝒜.left_inv x, ← sum_support_of _ (Decomposition.decompose' x),
  map_sum]
Proof state after:
case a.refine'_1.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' : r a b
h : x + b = a
⊢ ∑ x_1 ∈ DFinsupp.support (Decomposition.decompose' x),
      (DirectSum.coeAddMonoidHom 𝒜) ((of (fun i => ↥(𝒜 i)) x_1) ((Decomposition.decompose' x) x_1)) ∈
    Ideal.ofRel r'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_1.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' : r a b
h : x + b = a
⊢ ∑ x_1 ∈ DFinsupp.support (Decomposition.decompose' x),
      (DirectSum.coeAddMonoidHom 𝒜) ((of (fun i => ↥(𝒜 i)) x_1) ((Decomposition.decompose' x) x_1)) ∈
    Ideal.ofRel r'
Tactic:
apply Ideal.sum_mem
Proof state after:
case a.refine'_1.intro.intro.intro.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 a b : A
h' : r a b
h : x + b = a
⊢ ∀ c ∈ DFinsupp.support (Decomposition.decompose' x),
    (DirectSum.coeAddMonoidHom 𝒜) ((of (fun i => ↥(𝒜 i)) c) ((Decomposition.decompose' x) c)) ∈ Ideal.ofRel r'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_1.intro.intro.intro.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 a b : A
h' : r a b
h : x + b = a
⊢ ∀ c ∈ DFinsupp.support (Decomposition.decompose' x),
    (DirectSum.coeAddMonoidHom 𝒜) ((of (fun i => ↥(𝒜 i)) c) ((Decomposition.decompose' x) c)) ∈ Ideal.ofRel r'
Tactic:
intro i _
Proof state after:
case a.refine'_1.intro.intro.intro.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 a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ (DirectSum.coeAddMonoidHom 𝒜) ((of (fun i => ↥(𝒜 i)) i) ((Decomposition.decompose' x) i)) ∈ Ideal.ofRel r'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_1.intro.intro.intro.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 a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ (DirectSum.coeAddMonoidHom 𝒜) ((of (fun i => ↥(𝒜 i)) i) ((Decomposition.decompose' x) i)) ∈ Ideal.ofRel r'
Tactic:
rw [coeAddMonoidHom_of]
Proof state after:
case a.refine'_1.intro.intro.intro.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 a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ ↑((Decomposition.decompose' x) i) ∈ Ideal.ofRel r'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_1.intro.intro.intro.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 a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ ↑((Decomposition.decompose' x) i) ∈ Ideal.ofRel r'
Tactic:
apply Ideal.subset_span
Proof state after:
case a.refine'_1.intro.intro.intro.a.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 a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ ↑((Decomposition.decompose' x) i) ∈ {x | ∃ a b, r' a b ∧ x + b = a}
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case a.refine'_1.intro.intro.intro.a.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 a b : A
h' : r a b
h : x + b = a
i : ι
a✝ : i ∈ DFinsupp.support (Decomposition.decompose' x)
⊢ ↑((Decomposition.decompose' x) i) ∈ {x | ∃ a b, r' a b ∧ x + b = a}
Tactic:
use h𝒜.decompose' a 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)
⊢ ∃ b,
    r' (↑((Decomposition.decompose' a) i)) b ∧ ↑((Decomposition.decompose' x) i) + b = ↑((Decomposition.decompose' a) 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)
⊢ ∃ b,
    r' (↑((Decomposition.decompose' a) i)) b ∧ ↑((Decomposition.decompose' x) i) + b = ↑((Decomposition.decompose' a) i)
Tactic:
use h𝒜.decompose' b 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)
⊢ r' ↑((Decomposition.decompose' a) i) ↑((Decomposition.decompose' b) i) ∧
    ↑((Decomposition.decompose' x) i) + ↑((Decomposition.decompose' b) i) = ↑((Decomposition.decompose' a) 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' ↑((Decomposition.decompose' a) i) ↑((Decomposition.decompose' b) i) ∧
    ↑((Decomposition.decompose' x) i) + ↑((Decomposition.decompose' b) i) = ↑((Decomposition.decompose' a) i)
Tactic:
constructor
Proof state after:
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)

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)
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)

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:
. use i
  simp only [Decomposition.decompose'_eq, SetLike.coe_mem, true_and]
  simp only [Rel.IsHomogeneous] at hr
  exact hr h' i
Proof state after:
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)
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