Theorem: Ideal.IsHomogeneous_of_rel_isPureHomogeneous (DividedPowers/ForMathlib/GradedRingQuot.lean)

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

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

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

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

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

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
State after:
no goals