internlm/Lean-Github huggingface dataset:
Theorem: RingConGen.RelIsHomogeneous_of
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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
hn : ¬i + j = n
⊢ Rel rel
    (({ toFun := fun x => { toFun := fun y => 0, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) a) i))
      (((decomposeAlgEquiv 𝒜) c) j))
    (({ toFun := fun x => { toFun := fun y => 0, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) b) i))
      (((decomposeAlgEquiv 𝒜) d) j))
Tactic:
exact RingConGen.Rel.refl _
Proof state after:
no goals
Theorem: Ideal.IsHomogeneous_of_rel_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
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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
⊢ Ideal.IsHomogeneous 𝒜 (Ideal.ofRel r)
Tactic:
apply Ideal.homogeneous_span
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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
⊢ ∀ x ∈ {x | ∃ a b, r a b ∧ x + b = a}, SetLike.Homogeneous 𝒜 x
Theorem: Ideal.IsHomogeneous_of_rel_isPureHomogeneous
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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
⊢ ∀ x ∈ {x | ∃ a b, r a b ∧ x + b = a}, SetLike.Homogeneous 𝒜 x
Tactic:
rintro x  ⟨a, b, ⟨h, heq⟩⟩
Proof state after:
case h.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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
x a b : A
h : r a b
heq : x + b = a
⊢ SetLike.Homogeneous 𝒜 x
Theorem: Ideal.IsHomogeneous_of_rel_isPureHomogeneous
Proof state before:
case h.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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
x a b : A
h : r a b
heq : x + b = a
⊢ SetLike.Homogeneous 𝒜 x
Tactic:
obtain ⟨i, hi⟩ := hr h
Proof state after:
case h.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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
x a b : A
h : r a b
heq : x + b = a
i : ι
hi : a ∈ 𝒜 i ∧ b ∈ 𝒜 i
⊢ SetLike.Homogeneous 𝒜 x
Theorem: Ideal.IsHomogeneous_of_rel_isPureHomogeneous
Proof state before:
case h.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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
x a b : A
h : r a b
heq : x + b = a
i : ι
hi : a ∈ 𝒜 i ∧ b ∈ 𝒜 i
⊢ SetLike.Homogeneous 𝒜 x
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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
x a b : A
h : r a b
heq : x + b = a
i : ι
hi : a ∈ 𝒜 i ∧ b ∈ 𝒜 i
⊢ x ∈ 𝒜 i
Theorem: Ideal.IsHomogeneous_of_rel_isPureHomogeneous
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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
x a b : A
h : r a b
heq : x + b = a
i : ι
hi : a ∈ 𝒜 i ∧ b ∈ 𝒜 i
⊢ x ∈ 𝒜 i
Tactic:
rw [(eq_sub_iff_add_eq).mpr heq]
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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
x a b : A
h : r a b
heq : x + b = a
i : ι
hi : a ∈ 𝒜 i ∧ b ∈ 𝒜 i
⊢ a - b ∈ 𝒜 i
Theorem: Ideal.IsHomogeneous_of_rel_isPureHomogeneous
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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsPureHomogeneous 𝒜 r
x a b : A
h : r a b
heq : x + b = a
i : ι
hi : a ∈ 𝒜 i ∧ b ∈ 𝒜 i
⊢ a - b ∈ 𝒜 i
Tactic:
exact Submodule.sub_mem _ hi.1 hi.2
Proof state after:
no goals
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
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
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
⊢ Ideal.IsHomogeneous 𝒜 (Ideal.ofRel r)
Tactic:
let r' : A → A → Prop := fun a b => ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
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
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.IsHomogeneous 𝒜 (Ideal.ofRel r)
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
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
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.IsHomogeneous 𝒜 (Ideal.ofRel r)
Tactic:
suffices Ideal.ofRel r = Ideal.ofRel r' by
  rw [this]
  apply Ideal.IsHomogeneous_of_rel_isPureHomogeneous
  rintro a b ⟨i, h⟩
  exact ⟨i, h.1, h.2.1⟩
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
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'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
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
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:
apply le_antisymm
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
⊢ Ideal.ofRel r ≤ Ideal.ofRel r'

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

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
  refine' Submodule.span_induction hx _ _ _ _
  . 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]
  . simp only [Submodule.zero_mem]
  . intro x y hx hy
    exact Ideal.add_mem _ hx hy
  . intro a x hx
    simp only [smul_eq_mul]
    apply Ideal.mul_mem_left _ _ 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
⊢ Ideal.ofRel r' ≤ 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
⊢ Ideal.ofRel r' ≤ Ideal.ofRel r
Tactic:
. intro x hx'
  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)
  . 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:
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
this : Ideal.ofRel r = Ideal.ofRel r'
⊢ Ideal.IsHomogeneous 𝒜 (Ideal.ofRel r)
Tactic:
rw [this]
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
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
this : Ideal.ofRel r = Ideal.ofRel r'
⊢ Ideal.IsHomogeneous 𝒜 (Ideal.ofRel r')
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
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
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
this : Ideal.ofRel r = Ideal.ofRel r'
⊢ Ideal.IsHomogeneous 𝒜 (Ideal.ofRel r')
Tactic:
apply Ideal.IsHomogeneous_of_rel_isPureHomogeneous
Proof state after:
case hr
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
this : Ideal.ofRel r = Ideal.ofRel r'
⊢ Rel.IsPureHomogeneous 𝒜 r'
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case hr
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
this : Ideal.ofRel r = Ideal.ofRel r'
⊢ Rel.IsPureHomogeneous 𝒜 r'
Tactic:
rintro a b ⟨i, h⟩
Proof state after:
case hr.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
this : Ideal.ofRel r = Ideal.ofRel r'
a b : A
i : ι
h : a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
⊢ ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i
Theorem: Ideal.IsHomogeneous_of_rel_isHomogeneous
Proof state before:
case hr.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
this : Ideal.ofRel r = Ideal.ofRel r'
a b : A
i : ι
h : a ∈ 𝒜 i ∧ b ∈ 𝒜 i ∧ r a b
⊢ ∃ i, a ∈ 𝒜 i ∧ b ∈ 𝒜 i
Tactic:
exact ⟨i, h.1, h.2.1⟩
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'