-- Mathlib/RingTheory/GradedAlgebra/Radical.lean
theorem Ideal.IsHomogeneous.radical_eq {I : Ideal A} (hI : I.IsHomogeneous 𝒜) :
    I.radical = InfSet.sInf { J | Ideal.IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime }

Proof state:
case a
ι : 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
hI : IsHomogeneous 𝒜 I
⊢ ∀ x ∈ {J | I ≤ J ∧ J.IsPrime}, ∃ y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}, y ≤ x

Tactic:
rintro J ⟨HJ₁, HJ₂⟩

Result:
case a.intro
ι : 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
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ ∃ y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}, y ≤ J

Proof state:
case a
ι : 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
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

Tactic:
exact sInf_le_sInf fun J => And.right

Result:
no goals

Proof state:
case a.intro
ι : 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
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ (homogeneousCore 𝒜 J).toIdeal ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

Tactic:
refine ⟨HomogeneousIdeal.isHomogeneous _, ?_, HJ₂.homogeneousCore⟩

Result:
case a.intro
ι : 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
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ I ≤ (homogeneousCore 𝒜 J).toIdeal

Proof state:
case a.intro
ι : 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
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ ∃ y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}, y ≤ J

Tactic:
refine ⟨(J.homogeneousCore 𝒜).toIdeal, ?_, J.toIdeal_homogeneousCore_le _⟩

Result:
case a.intro
ι : 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
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ (homogeneousCore 𝒜 J).toIdeal ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.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
hI : IsHomogeneous 𝒜 I
⊢ I.radical = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

Tactic:
rw [Ideal.radical_eq_sInf]

Result:
ι : 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
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ J.IsPrime} = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

Proof state:
case a.intro
ι : 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
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ I ≤ (homogeneousCore 𝒜 J).toIdeal

Tactic:
exact hI.toIdeal_homogeneousCore_eq_self.symm.trans_le (Ideal.homogeneousCore_mono _ HJ₁)

Result:
no goals

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
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ J.IsPrime} = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

Tactic:
apply le_antisymm

Result:
case a
ι : 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
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

case a
ι : 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
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | I ≤ J ∧ J.IsPrime}

Proof state:
case a
ι : 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
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | I ≤ J ∧ J.IsPrime}

Tactic:
refine sInf_le_sInf_of_forall_exists_le ?_

Result:
case a
ι : 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
hI : IsHomogeneous 𝒜 I
⊢ ∀ x ∈ {J | I ≤ J ∧ J.IsPrime}, ∃ y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}, y ≤ x