case I_ne_top
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
⊢ (Ideal.homogeneousCore 𝒜 I).toSubmodule ≠ ⊤

case homogeneous_mem_or_mem
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
⊢ ∀ {x y : A},
    Homogeneous 𝒜 x →
      Homogeneous 𝒜 y →
        x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule →
          x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
⊢ IsPrime (HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I))
apply (Ideal.homogeneousCore 𝒜 I).is_homogeneous'.isPrime_of_homogeneous_mem_or_mem
case homogeneous_mem_or_mem
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
case homogeneous_mem_or_mem
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
⊢ ∀ {x y : A},
    Homogeneous 𝒜 x →
      Homogeneous 𝒜 y →
        x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule →
          x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
rintro x y hx hy hxy
case homogeneous_mem_or_mem
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
H : x ∈ I ∨ y ∈ I
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
case homogeneous_mem_or_mem
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
have H := h.mem_or_mem (Ideal.toIdeal_homogeneousCore_le 𝒜 I hxy)
case homogeneous_mem_or_mem.refine'_1
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
H : x ∈ I ∨ y ∈ I
⊢ x ∈ I → x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule

case homogeneous_mem_or_mem.refine'_2
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
case homogeneous_mem_or_mem
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
H : x ∈ I ∨ y ∈ I
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
refine' H.imp _ _
no goals
case I_ne_top
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
⊢ (Ideal.homogeneousCore 𝒜 I).toSubmodule ≠ ⊤
exact ne_top_of_le_ne_top h.ne_top (Ideal.toIdeal_homogeneousCore_le 𝒜 I)
no goals
case homogeneous_mem_or_mem.refine'_1
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
H : x ∈ I ∨ y ∈ I
⊢ x ∈ I → x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hx
no goals
case homogeneous_mem_or_mem.refine'_2
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hy