-- Mathlib/RingTheory/GradedAlgebra/Radical.lean
theorem Ideal.IsPrime.homogeneousCore {I : Ideal A} (h : I.IsPrime) :
    (I.homogeneousCore 𝒜).toIdeal.IsPrime

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
⊢ (Ideal.homogeneousCore 𝒜 I).toIdeal.IsPrime

Tactic:
apply (Ideal.homogeneousCore 𝒜 I).isHomogeneous.isPrime_of_homogeneous_mem_or_mem

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

case homogeneous_mem_or_mem
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
⊢ ∀ {x y : A},
    IsHomogeneousElem 𝒜 x →
      IsHomogeneousElem 𝒜 y →
        x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal →
          x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Proof state:
case homogeneous_mem_or_mem
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
⊢ ∀ {x y : A},
    IsHomogeneousElem 𝒜 x →
      IsHomogeneousElem 𝒜 y →
        x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal →
          x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Tactic:
rintro x y hx hy hxy

Result:
case homogeneous_mem_or_mem
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Proof state:
case homogeneous_mem_or_mem.refine_1
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ x ∈ I → x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Tactic:
exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hx

Result:
no goals

Proof state:
case homogeneous_mem_or_mem.refine_2
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Tactic:
exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hy

Result:
no goals

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

Tactic:
exact ne_top_of_le_ne_top h.ne_top (Ideal.toIdeal_homogeneousCore_le 𝒜 I)

Result:
no goals

Proof state:
case homogeneous_mem_or_mem
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Tactic:
refine H.imp ?_ ?_

Result:
case homogeneous_mem_or_mem.refine_1
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ x ∈ I → x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

case homogeneous_mem_or_mem.refine_2
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Proof state:
case homogeneous_mem_or_mem
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Tactic:
have H := h.mem_or_mem (Ideal.toIdeal_homogeneousCore_le 𝒜 I hxy)

Result:
case homogeneous_mem_or_mem
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal