-- Mathlib/RingTheory/GradedAlgebra/Radical.lean
theorem Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem {I : Ideal A} (hI : I.IsHomogeneous 𝒜)
    (I_ne_top : I ≠ ⊤)
    (homogeneous_mem_or_mem :
      ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I) :
    Ideal.IsPrime I :=
  ⟨I_ne_top, by
    intro x y hxy
    by_contra! rid
    obtain ⟨rid₁, rid₂⟩ := rid
    classical
      /-
        The idea of the proof is the following :
        since `x * y ∈ I` and `I` homogeneous, then `proj i (x * y) ∈ I` for any `i : ι`.
        Then consider two sets `{i ∈ x.support | xᵢ ∉ I}` and `{j ∈ y.support | yⱼ ∉ J}`;
        let `max₁, max₂` be the maximum of the two sets, then `proj (max₁ + max₂) (x * y) ∈ I`.
        Then, `proj max₁ x ∉ I` and `proj max₂ j ∉ I`
        but `proj i x ∈ I` for all `max₁ < i` and `proj j y ∈ I` for all `max₂ < j`.
        `  proj (max₁ + max₂) (x * y)`
        `= ∑ {(i, j) ∈ supports | i + j = max₁ + max₂}, xᵢ * yⱼ`
        `= proj max₁ x * proj max₂ y`
        `  + ∑ {(i, j) ∈ supports \ {(max₁, max₂)} | i + j = max₁ + max₂}, xᵢ * yⱼ`.
        This is a contradiction, because both `proj (max₁ + max₂) (x * y) ∈ I` and the sum on the
        right hand side is in `I` however `proj max₁ x * proj max₂ y` is not in `I`.
        -/
      set set₁ := {i ∈ (decompose 𝒜 x).support | proj 𝒜 i x ∉ I} with set₁_eq
      set set₂ := {i ∈ (decompose 𝒜 y).support | proj 𝒜 i y ∉ I} with set₂_eq
      have nonempty :
        ∀ x : A, x ∉ I → {i ∈ (decompose 𝒜 x).support | proj 𝒜 i x ∉ I}.Nonempty

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_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))
set₁_eq : set₁ = filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))
set₂ : Finset ι := filter (fun i => (proj 𝒜 i) y ∉ I) (DFinsupp.support ((decompose 𝒜) y))
set₂_eq : set₂ = filter (fun i => (proj 𝒜 i) y ∉ I) (DFinsupp.support ((decompose 𝒜) y))
nonempty : ∀ x ∉ I, (filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))).Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.1 + z.2 = max₁ + max₂) (DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.1 + z.2 = max₁ + max₂) (DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y))
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
z : ι × ι
H : z ∈ antidiag.erase (max₁, max₂)
⊢ (proj 𝒜 z.1) x * (proj 𝒜 z.2) y ∈ I

Tactic:
rcases z with ⟨i, j⟩

Result:
case mk
ι : 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_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))
set₁_eq : set₁ = filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))
set₂ : Finset ι := filter (fun i => (proj 𝒜 i) y ∉ I) (DFinsupp.support ((decompose 𝒜) y))
set₂_eq : set₂ = filter (fun i => (proj 𝒜 i) y ∉ I) (DFinsupp.support ((decompose 𝒜) y))
nonempty : ∀ x ∉ I, (filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))).Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.1 + z.2 = max₁ + max₂) (DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.1 + z.2 = max₁ + max₂) (DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y))
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
i j : ι
H : (i, j) ∈ antidiag.erase (max₁, max₂)
⊢ (proj 𝒜 (i, j).1) x * (proj 𝒜 (i, j).2) y ∈ I

Proof state:
case 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
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))
set₁_eq : set₁ = filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))
set₂ : Finset ι := filter (fun i => (proj 𝒜 i) y ∉ I) (DFinsupp.support ((decompose 𝒜) y))
set₂_eq : set₂ = filter (fun i => (proj 𝒜 i) y ∉ I) (DFinsupp.support ((decompose 𝒜) y))
nonempty : ∀ x ∉ I, (filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))).Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
mem_I : (proj 𝒜 max₁) x * (proj 𝒜 max₂) y ∈ I
not_mem_I : (proj 𝒜 max₁) x * (proj 𝒜 max₂) y ∉ I
⊢ False

Tactic:
exact not_mem_I mem_I

Result:
no goals

Proof state:
case inl
ι : 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_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))
set₁_eq : set₁ = filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))
set₂ : Finset ι := filter (fun i => (proj 𝒜 i) y ∉ I) (DFinsupp.support ((decompose 𝒜) y))
set₂_eq : set₂ = filter (fun i => (proj 𝒜 i) y ∉ I) (DFinsupp.support ((decompose 𝒜) y))
nonempty : ∀ x ∉ I, (filter (fun i => (proj 𝒜 i) x ∉ I) (DFinsupp.support ((decompose 𝒜) x))).Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
mem_I : (proj 𝒜 max₁) x * (proj 𝒜 max₂) y ∈ I
neither_mem : (proj 𝒜 max₁) x ∉ I ∧ (proj 𝒜 max₂) y ∉ I
_rid : (proj 𝒜 max₁) x * (proj 𝒜 max₂) y ∈ I
h : ↑(((DFinsupp.evalAddMonoidHom max₁).comp (decomposeRingEquiv 𝒜).toRingHom.toAddMonoidHom) x) ∈ I
⊢ False

Tactic:
apply neither_mem.1 h

Result:
no goals