awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ I.IsPrime ↔ I ≠ ⊤ ∧ ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
⟨fun HI => ⟨HI.ne_top, fun _ _ hxy => Ideal.IsPrime.mem_or_mem HI hxy⟩,
    fun ⟨I_ne_top, homogeneous_mem_or_mem⟩ =>
    h.isPrime_of_homogeneous_mem_or_mem I_ne_top @homogeneous_mem_or_mem⟩

Premises used: _private.0.Ideal.IsHomogeneous.isPrime_iff.match_1, Ideal.IsPrime.mem_or_mem, Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem, And.intro, Iff.intro, Ideal.IsPrime, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
I_ne_top : HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I) ≠ ⊤
homogeneous_mem_or_mem :
  ∀ {x y : A},
    IsHomogeneousElem 𝒜 x →
      IsHomogeneousElem 𝒜 y →
        x * y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I) →
          x ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I) ∨
            y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
⊢ (HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)).IsPrime

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

Premises used: HomogeneousIdeal.isHomogeneous, Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem, Ideal.homogeneousCore
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
⊢ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I) ≠ ⊤

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

Premises used: ne_top_of_le_ne_top, Ideal.IsPrime.ne_top, Ideal.toIdeal_homogeneousCore_le
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
⊢ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I) ≠ ⊤

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

Premises used: ne_top_of_le_ne_top, Ideal.IsPrime.ne_top, Ideal.toIdeal_homogeneousCore_le
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
⊢ x ∈ I ∨ y ∈ I

Tactic:
have H := h.mem_or_mem (Ideal.toIdeal_homogeneousCore_le 𝒜 I hxy)
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
H : x ∈ I ∨ y ∈ I
⊢ x ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I) ∨ y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)

Tactic:
H.imp ?_ ?_

Premises used: Or.imp
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
H : x ∈ I ∨ y ∈ I
homogeneous_mem_or_mem : x ∈ I → x ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
homogeneous_mem_or_mem₁ : y ∈ I → y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
⊢ x ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I) ∨ y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)

Tactic:
refine H.imp ?_ ?_

Premises used: Or.imp
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
H : x ∈ I ∨ y ∈ I
⊢ x ∈ I → x ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)

Tactic:
Ideal.mem_homogeneousCore_of_homogeneous_of_mem hx

Premises used: Set.Mem, Ideal.mem_homogeneousCore_of_homogeneous_of_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
H : x ∈ I ∨ y ∈ I
⊢ x ∈ I → x ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)

Tactic:
exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hx

Premises used: Ideal.mem_homogeneousCore_of_homogeneous_of_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)

Tactic:
Ideal.mem_homogeneousCore_of_homogeneous_of_mem hy

Premises used: Set.Mem, Ideal.mem_homogeneousCore_of_homogeneous_of_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I)

Tactic:
exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hy

Premises used: Ideal.mem_homogeneousCore_of_homogeneous_of_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
rw :
  Eq.{u_3 + 1} (α := Ideal A) (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
⊢ I.radical = InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

Tactic:
rw [Ideal.radical_eq_sInf]

Premises used: Ideal.radical_eq_sInf
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
a :
  LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
a₁ :
  LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
⊢ Eq.{u_3 + 1} (α := Ideal A) (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})

Tactic:
sInf_le_sInf fun J => And.right

Premises used: Set.Mem, sInf_le_sInf, And.right
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})

Tactic:
exact sInf_le_sInf fun J => And.right

Premises used: sInf_le_sInf, And.right
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})

Tactic:
sInf_le_sInf_of_isCoinitialFor ?_

Premises used: Set.Mem, sInf_le_sInf_of_isCoinitialFor
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
a :
  IsCoinitialFor.{u_3} (α := Ideal A) {J : Ideal A | I ≤ J ∧ J.IsPrime}
    {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
⊢ LE.le.{u_3} (α := Ideal A) (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
    (InfSet.sInf {J : Ideal A | I ≤ J ∧ J.IsPrime})

Tactic:
refine sInf_le_sInf_of_isCoinitialFor ?_

Premises used: sInf_le_sInf_of_isCoinitialFor
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ ∃ (b : Ideal A), Membership.mem (γ := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} b ∧ b ≤ J

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

Premises used: And.intro, Exists.intro, Ideal.homogeneousCore, HomogeneousIdeal.toIdeal, Ideal.toIdeal_homogeneousCore_le
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
a :
  Membership.mem (γ := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
    (HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J))
⊢ ∃ (b : Ideal A), Membership.mem (γ := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} b ∧ b ≤ J

Tactic:
refine ⟨(J.homogeneousCore 𝒜).toIdeal, ?_, J.toIdeal_homogeneousCore_le _⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ Membership.mem (γ := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
    (HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J))

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

Premises used: Set.Mem, setOf, HomogeneousIdeal.isHomogeneous, Ideal.IsPrime.homogeneousCore, And.intro
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
a : I ≤ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J)
⊢ Membership.mem (γ := Set (Ideal A)) {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
    (HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J))

Tactic:
refine ⟨HomogeneousIdeal.isHomogeneous _, ?_, HJ₂.homogeneousCore⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ I ≤ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J)

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

Premises used: Eq.trans_le, Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self, Ideal.homogeneousCore_mono, Eq.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ I ≤ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J)

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

Premises used: Eq.trans_le, Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self, Ideal.homogeneousCore_mono, Eq.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
rw : IsHomogeneous 𝒜 (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
⊢ IsHomogeneous 𝒜 I.radical

Tactic:
rw [h.radical_eq]

Premises used: Ideal.IsHomogeneous.radical_eq
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})

Tactic:
Ideal.IsHomogeneous.sInf fun _ => And.left

Premises used: Ideal.IsHomogeneous.sInf, And.left
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf {J : Ideal A | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})

Tactic:
exact Ideal.IsHomogeneous.sInf fun _ => And.left

Premises used: Ideal.IsHomogeneous.sInf, And.left
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ I.radical.toIdeal = I.toIdeal.radical

Tactic:
rfl

Premises used: Ideal.radical, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
f g : 𝒜 →+*ᵍ ℬ
h :
  Eq (α := (a : A) → B) ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) f)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)
mk :
  ∀ (toRingHom : A →+* B)
    (map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B))
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
          { toRingHom := toRingHom, map_mem := @map_mem })
        ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)),
    { toRingHom := toRingHom, map_mem := @map_mem : 𝒜 →+*ᵍ ℬ } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
g : 𝒜 →+*ᵍ ℬ
toRingHom : A →+* B
map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B)
h :
  Eq (α := (a : A) → B)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom, map_mem := @map_mem })
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)
mk :
  ∀ (toRingHom_1 : A →+* B)
    (map_mem_1 :
      ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom_1 : (a : A) → B) x : B))
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
          { toRingHom := toRingHom, map_mem := @map_mem })
        ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
          { toRingHom := toRingHom_1, map_mem := @map_mem_1 })),
    { toRingHom := toRingHom, map_mem := @map_mem : 𝒜 →+*ᵍ ℬ } = { toRingHom := toRingHom_1, map_mem := @map_mem_1 }
⊢ { toRingHom := toRingHom, map_mem := @map_mem : 𝒜 →+*ᵍ ℬ } = g

Tactic:
cases g
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
toRingHom : A →+* B
map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B)
toRingHom_1 : A →+* B
map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom_1 : (a : A) → B) x : B)
h :
  Eq (α := (a : A) → B)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom, map_mem := @map_mem })
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom_1, map_mem := @map_mem_1 })
mk : toRingHom = toRingHom_1
⊢ { toRingHom := toRingHom, map_mem := @map_mem : 𝒜 →+*ᵍ ℬ } = { toRingHom := toRingHom_1, map_mem := @map_mem_1 }

Tactic:
congr
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
toRingHom : A →+* B
map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B)
toRingHom_1 : A →+* B
map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom_1 : (a : A) → B) x : B)
h :
  Eq (α := (a : A) → B)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom, map_mem := @map_mem })
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom_1, map_mem := @map_mem_1 })
mk : Eq (α := (a : A) → B) (⇑toRingHom : (a : A) → B) (⇑toRingHom_1 : (a : A) → B)
⊢ toRingHom = toRingHom_1

Tactic:
apply DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
toRingHom : A →+* B
map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B)
toRingHom_1 : A →+* B
map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom_1 : (a : A) → B) x : B)
h :
  Eq (α := (a : A) → B)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom, map_mem := @map_mem })
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom_1, map_mem := @map_mem_1 })
⊢ Eq (α := (a : A) → B) (⇑toRingHom : (a : A) → B) (⇑toRingHom_1 : (a : A) → B)

Tactic:
h
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
σ : Type u_6
τ : Type u_7
ψ : Type u_8
ω : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Semiring D
inst_4 : SetLike σ A
inst_5 : SetLike τ B
inst_6 : SetLike ψ C
inst_7 : SetLike ω D
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
𝒟 : ι → ω
toRingHom : A →+* B
map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom : (a : A) → B) x : B)
toRingHom_1 : A →+* B
map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → Membership.mem.{u_3, u_7} (α := B) (ℬ i) ((toRingHom_1 : (a : A) → B) x : B)
h :
  Eq (α := (a : A) → B)
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom, map_mem := @map_mem })
    ((fun (f : 𝒜 →+*ᵍ ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toRingHom := toRingHom_1, map_mem := @map_mem_1 })
⊢ Eq (α := (a : A) → B) (⇑toRingHom : (a : A) → B) (⇑toRingHom_1 : (a : A) → B)

Tactic:
exact h
-- Module: Mathlib.RingTheory.GradedAlgebra.RingHom
Goal:
ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst : Semiring A
inst_1 : Semiring B
inst_2 : SetLike σ A
inst_3 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
f : 𝒜 →+*ᵍ ℬ
⊢ (↑f : A →+* B) = (↑f : A →+* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl