-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem Ideal.homogeneousCore'_eq_sSup :
    I.homogeneousCore' 𝒜 = sSup { J : Ideal A | J.IsHomogeneous 𝒜 ∧ J ≤ I }

Proof state:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
⊢ IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)

Tactic:
convert coe_mono.map_isGreatest (Ideal.homogeneousCore.gc 𝒜).isGreatest_u using 1

Result:
case h.e'_3
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
⊢ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} = toIdeal '' {a | a.toIdeal ≤ I}

Proof state:
case h.e'_3.h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ IsHomogeneous 𝒜 x ∧ x ≤ I ↔ ∃ x_1 ∈ {a | a.toIdeal ≤ I}, x_1.toIdeal = x

Tactic:
refine ⟨fun hI => ⟨⟨x, hI.1⟩, ⟨hI.2, rfl⟩⟩, ?_⟩

Result:
case h.e'_3.h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ (∃ x_1 ∈ {a | a.toIdeal ≤ I}, x_1.toIdeal = x) → IsHomogeneous 𝒜 x ∧ x ≤ I

Proof state:
case h.e'_3
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
⊢ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} = toIdeal '' {a | a.toIdeal ≤ I}

Tactic:
ext x

Result:
case h.e'_3.h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ x ∈ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} ↔ x ∈ toIdeal '' {a | a.toIdeal ≤ I}

Proof state:
case h.e'_3.h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ (∃ x_1 ∈ {a | a.toIdeal ≤ I}, x_1.toIdeal = x) → IsHomogeneous 𝒜 x ∧ x ≤ I

Tactic:
rintro ⟨x, ⟨hx, rfl⟩⟩

Result:
case h.e'_3.h.intro.intro
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : HomogeneousIdeal 𝒜
hx : x ∈ {a | a.toIdeal ≤ I}
⊢ IsHomogeneous 𝒜 x.toIdeal ∧ x.toIdeal ≤ I

Proof state:
case h.e'_3.h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ x ∈ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} ↔ x ∈ toIdeal '' {a | a.toIdeal ≤ I}

Tactic:
rw [mem_image, mem_setOf_eq]

Result:
case h.e'_3.h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ IsHomogeneous 𝒜 x ∧ x ≤ I ↔ ∃ x_1 ∈ {a | a.toIdeal ≤ I}, x_1.toIdeal = x

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsLUB {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)

Tactic:
apply IsGreatest.isLUB

Result:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ homogeneousCore' 𝒜 I = sSup {J | IsHomogeneous 𝒜 J ∧ J ≤ I}

Tactic:
refine (IsLUB.sSup_eq ?_).symm

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsLUB {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)

Proof state:
case h.e'_3.h.intro.intro
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : HomogeneousIdeal 𝒜
hx : x ∈ {a | a.toIdeal ≤ I}
⊢ IsHomogeneous 𝒜 x.toIdeal ∧ x.toIdeal ≤ I

Tactic:
exact ⟨x.isHomogeneous, hx⟩

Result:
no goals

Proof state:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)

Tactic:
have coe_mono : Monotone (toIdeal : HomogeneousIdeal 𝒜 → Ideal A) := fun x y => id

Result:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
⊢ IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)