[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : A}, x * y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
intro x y hxy
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
[PROOFSTEP]
by_contra rid
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
rid : ¬(x ∈ I ∨ y ∈ I)
⊢ False
[PROOFSTEP]
push_neg at rid 
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
rid : ¬x ∈ I ∧ ¬y ∈ I
⊢ False
[PROOFSTEP]
obtain ⟨rid₁, rid₂⟩ := rid
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
rid₁ : ¬x ∈ I
rid₂ : ¬y ∈ I
⊢ False
[PROOFSTEP]
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₁ := (decompose 𝒜 x).support.filter (fun i => proj 𝒜 i x ∉ I) with set₁_eq
set set₂ := (decompose 𝒜 y).support.filter (fun i => proj 𝒜 i y ∉ I) with set₂_eq
have nonempty : ∀ x : A, x ∉ I → ((decompose 𝒜 x).support.filter (fun i => proj 𝒜 i x ∉ I)).Nonempty :=
  by
  intro x hx
  rw [filter_nonempty_iff]
  contrapose! hx
  simp_rw [proj_apply] at hx 
  rw [← sum_support_decompose 𝒜 x]
  exact Ideal.sum_mem _ hx
set max₁ := set₁.max' (nonempty x rid₁)
set max₂ := set₂.max' (nonempty y rid₂)
have mem_max₁ : max₁ ∈ set₁ := max'_mem set₁ (nonempty x rid₁)
have mem_max₂ : max₂ ∈ set₂ := max'_mem set₂ (nonempty y rid₂)
replace hxy : proj 𝒜 (max₁ + max₂) (x * y) ∈ I := hI _ hxy
have mem_I : proj 𝒜 max₁ x * proj 𝒜 max₂ y ∈ I :=
  by
  set antidiag :=
    ((decompose 𝒜 x).support ×ˢ (decompose 𝒜 y).support).filter (fun z : ι × ι => z.1 + z.2 = max₁ + max₂) with ha
  have mem_antidiag : (max₁, max₂) ∈ antidiag :=
    by
    simp only [add_sum_erase, mem_filter, mem_product]
    exact ⟨⟨mem_of_mem_filter _ mem_max₁, mem_of_mem_filter _ mem_max₂⟩, trivial⟩
  have eq_add_sum :=
    calc
      proj 𝒜 (max₁ + max₂) (x * y) = ∑ ij in antidiag, proj 𝒜 ij.1 x * proj 𝒜 ij.2 y := by
        simp_rw [ha, proj_apply, DirectSum.decompose_mul, DirectSum.coe_mul_apply 𝒜]
      _ = proj 𝒜 max₁ x * proj 𝒜 max₂ y + ∑ ij in antidiag.erase (max₁, max₂), proj 𝒜 ij.1 x * proj 𝒜 ij.2 y :=
        (add_sum_erase _ _ mem_antidiag).symm
  rw [eq_sub_of_add_eq eq_add_sum.symm]
  refine' Ideal.sub_mem _ hxy (Ideal.sum_mem _ fun z H => _)
  rcases z with ⟨i, j⟩
  simp only [mem_erase, Prod.mk.inj_iff, Ne.def, mem_filter, mem_product] at H 
  rcases H with ⟨H₁, ⟨H₂, H₃⟩, H₄⟩
  have max_lt : max₁ < i ∨ max₂ < j :=
    by
    rcases lt_trichotomy max₁ i with (h | rfl | h)
    · exact Or.inl h
    · refine' False.elim (H₁ ⟨rfl, add_left_cancel H₄⟩)
    · apply Or.inr
      have := add_lt_add_right h j
      rw [H₄] at this 
      exact lt_of_add_lt_add_left this
  cases' max_lt with max_lt max_lt
  ·
    -- in this case `max₁ < i`, then `xᵢ ∈ I`; for otherwise `i ∈ set₁` then `i ≤ max₁`.
    have not_mem : i ∉ set₁ := fun h => lt_irrefl _ ((max'_lt_iff set₁ (nonempty x rid₁)).mp max_lt i h)
    rw [set₁_eq] at not_mem 
    simp only [not_and, Classical.not_not, Ne.def, mem_filter] at not_mem 
    exact Ideal.mul_mem_right _ I (not_mem H₂)
  ·
    -- in this case `max₂ < j`, then `yⱼ ∈ I`; for otherwise `j ∈ set₂`, then `j ≤ max₂`.
    have not_mem : j ∉ set₂ := fun h => lt_irrefl _ ((max'_lt_iff set₂ (nonempty y rid₂)).mp max_lt j h)
    rw [set₂_eq] at not_mem 
    simp only [not_and, Classical.not_not, Ne.def, mem_filter] at not_mem 
    exact Ideal.mul_mem_left I _ (not_mem H₃)
have not_mem_I : proj 𝒜 max₁ x * proj 𝒜 max₂ y ∉ I :=
  by
  have neither_mem : proj 𝒜 max₁ x ∉ I ∧ proj 𝒜 max₂ y ∉ I :=
    by
    rw [mem_filter] at mem_max₁ mem_max₂ 
    exact ⟨mem_max₁.2, mem_max₂.2⟩
  intro _rid
  cases' homogeneous_mem_or_mem ⟨max₁, SetLike.coe_mem _⟩ ⟨max₂, SetLike.coe_mem _⟩ mem_I with h h
  · apply neither_mem.1 h
  · apply neither_mem.2 h
exact not_mem_I mem_I
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
rid₁ : ¬x ∈ I
rid₂ : ¬y ∈ I
⊢ False
[PROOFSTEP]
set set₁ := (decompose 𝒜 x).support.filter (fun i => proj 𝒜 i x ∉ I) with set₁_eq
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
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))
⊢ False
[PROOFSTEP]
set set₂ := (decompose 𝒜 y).support.filter (fun i => proj 𝒜 i y ∉ I) with set₂_eq
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
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))
⊢ False
[PROOFSTEP]
have nonempty : ∀ x : A, x ∉ I → ((decompose 𝒜 x).support.filter (fun i => proj 𝒜 i x ∉ I)).Nonempty :=
  by
  intro x hx
  rw [filter_nonempty_iff]
  contrapose! hx
  simp_rw [proj_apply] at hx 
  rw [← sum_support_decompose 𝒜 x]
  exact Ideal.sum_mem _ hx
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
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))
⊢ ∀ (x : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
[PROOFSTEP]
intro x hx
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
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))
x : A
hx : ¬x ∈ I
⊢ Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
[PROOFSTEP]
rw [filter_nonempty_iff]
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
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))
x : A
hx : ¬x ∈ I
⊢ ∃ a, a ∈ DFinsupp.support (↑(decompose 𝒜) x) ∧ ¬↑(proj 𝒜 a) x ∈ I
[PROOFSTEP]
contrapose! hx
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
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))
x : A
hx : ∀ (a : ι), a ∈ DFinsupp.support (↑(decompose 𝒜) x) → ↑(proj 𝒜 a) x ∈ I
⊢ x ∈ I
[PROOFSTEP]
simp_rw [proj_apply] at hx 
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
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))
x : A
hx : ∀ (a : ι), a ∈ DFinsupp.support (↑(decompose 𝒜) x) → ↑(↑(↑(decompose 𝒜) x) a) ∈ I
⊢ x ∈ I
[PROOFSTEP]
rw [← sum_support_decompose 𝒜 x]
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
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))
x : A
hx : ∀ (a : ι), a ∈ DFinsupp.support (↑(decompose 𝒜) x) → ↑(↑(↑(decompose 𝒜) x) a) ∈ I
⊢ ∑ i in DFinsupp.support (↑(decompose 𝒜) x), ↑(↑(↑(decompose 𝒜) x) i) ∈ I
[PROOFSTEP]
exact Ideal.sum_mem _ hx
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
⊢ False
[PROOFSTEP]
set max₁ := set₁.max' (nonempty x rid₁)
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
⊢ False
[PROOFSTEP]
set max₂ := set₂.max' (nonempty y rid₂)
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
⊢ False
[PROOFSTEP]
have mem_max₁ : max₁ ∈ set₁ := max'_mem set₁ (nonempty x rid₁)
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
⊢ False
[PROOFSTEP]
have mem_max₂ : max₂ ∈ set₂ := max'_mem set₂ (nonempty y rid₂)
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
⊢ False
[PROOFSTEP]
replace hxy : proj 𝒜 (max₁ + max₂) (x * y) ∈ I := hI _ hxy
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
⊢ False
[PROOFSTEP]
have mem_I : proj 𝒜 max₁ x * proj 𝒜 max₂ y ∈ I :=
  by
  set antidiag :=
    ((decompose 𝒜 x).support ×ˢ (decompose 𝒜 y).support).filter (fun z : ι × ι => z.1 + z.2 = max₁ + max₂) with ha
  have mem_antidiag : (max₁, max₂) ∈ antidiag :=
    by
    simp only [add_sum_erase, mem_filter, mem_product]
    exact ⟨⟨mem_of_mem_filter _ mem_max₁, mem_of_mem_filter _ mem_max₂⟩, trivial⟩
  have eq_add_sum :=
    calc
      proj 𝒜 (max₁ + max₂) (x * y) = ∑ ij in antidiag, proj 𝒜 ij.1 x * proj 𝒜 ij.2 y := by
        simp_rw [ha, proj_apply, DirectSum.decompose_mul, DirectSum.coe_mul_apply 𝒜]
      _ = proj 𝒜 max₁ x * proj 𝒜 max₂ y + ∑ ij in antidiag.erase (max₁, max₂), proj 𝒜 ij.1 x * proj 𝒜 ij.2 y :=
        (add_sum_erase _ _ mem_antidiag).symm
  rw [eq_sub_of_add_eq eq_add_sum.symm]
  refine' Ideal.sub_mem _ hxy (Ideal.sum_mem _ fun z H => _)
  rcases z with ⟨i, j⟩
  simp only [mem_erase, Prod.mk.inj_iff, Ne.def, mem_filter, mem_product] at H 
  rcases H with ⟨H₁, ⟨H₂, H₃⟩, H₄⟩
  have max_lt : max₁ < i ∨ max₂ < j :=
    by
    rcases lt_trichotomy max₁ i with (h | rfl | h)
    · exact Or.inl h
    · refine' False.elim (H₁ ⟨rfl, add_left_cancel H₄⟩)
    · apply Or.inr
      have := add_lt_add_right h j
      rw [H₄] at this 
      exact lt_of_add_lt_add_left this
  cases' max_lt with max_lt max_lt
  ·
    -- in this case `max₁ < i`, then `xᵢ ∈ I`; for otherwise `i ∈ set₁` then `i ≤ max₁`.
    have not_mem : i ∉ set₁ := fun h => lt_irrefl _ ((max'_lt_iff set₁ (nonempty x rid₁)).mp max_lt i h)
    rw [set₁_eq] at not_mem 
    simp only [not_and, Classical.not_not, Ne.def, mem_filter] at not_mem 
    exact Ideal.mul_mem_right _ I (not_mem H₂)
  ·
    -- in this case `max₂ < j`, then `yⱼ ∈ I`; for otherwise `j ∈ set₂`, then `j ≤ max₂`.
    have not_mem : j ∉ set₂ := fun h => lt_irrefl _ ((max'_lt_iff set₂ (nonempty y rid₂)).mp max_lt j h)
    rw [set₂_eq] at not_mem 
    simp only [not_and, Classical.not_not, Ne.def, mem_filter] at not_mem 
    exact Ideal.mul_mem_left I _ (not_mem H₃)
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
⊢ ↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
[PROOFSTEP]
set antidiag :=
  ((decompose 𝒜 x).support ×ˢ (decompose 𝒜 y).support).filter (fun z : ι × ι => z.1 + z.2 = max₁ + max₂) with ha
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = max₁ + max₂)
      (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
⊢ ↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
[PROOFSTEP]
have mem_antidiag : (max₁, max₂) ∈ antidiag :=
  by
  simp only [add_sum_erase, mem_filter, mem_product]
  exact ⟨⟨mem_of_mem_filter _ mem_max₁, mem_of_mem_filter _ mem_max₂⟩, trivial⟩
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = max₁ + max₂)
      (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
⊢ (max₁, max₂) ∈ antidiag
[PROOFSTEP]
simp only [add_sum_erase, mem_filter, mem_product]
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = max₁ + max₂)
      (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
⊢ (max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∈
        DFinsupp.support (↑(decompose 𝒜) x) ∧
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))) ∈
        DFinsupp.support (↑(decompose 𝒜) y)) ∧
    True
[PROOFSTEP]
exact ⟨⟨mem_of_mem_filter _ mem_max₁, mem_of_mem_filter _ mem_max₂⟩, trivial⟩
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = max₁ + max₂)
      (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
mem_antidiag : (max₁, max₂) ∈ antidiag
⊢ ↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
[PROOFSTEP]
have eq_add_sum :=
  calc
    proj 𝒜 (max₁ + max₂) (x * y) = ∑ ij in antidiag, proj 𝒜 ij.1 x * proj 𝒜 ij.2 y := by
      simp_rw [ha, proj_apply, DirectSum.decompose_mul, DirectSum.coe_mul_apply 𝒜]
    _ = proj 𝒜 max₁ x * proj 𝒜 max₂ y + ∑ ij in antidiag.erase (max₁, max₂), proj 𝒜 ij.1 x * proj 𝒜 ij.2 y :=
      (add_sum_erase _ _ mem_antidiag).symm
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = max₁ + max₂)
      (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
mem_antidiag : (max₁, max₂) ∈ antidiag
⊢ ↑(proj 𝒜 (max₁ + max₂)) (x * y) = ∑ ij in antidiag, ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
[PROOFSTEP]
simp_rw [ha, proj_apply, DirectSum.decompose_mul, DirectSum.coe_mul_apply 𝒜]
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
⊢ ↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
[PROOFSTEP]
rw [eq_sub_of_add_eq eq_add_sum.symm]
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
⊢ ↑(proj 𝒜 (max₁ + max₂)) (x * y) - ∑ ij in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y ∈ I
[PROOFSTEP]
refine' Ideal.sub_mem _ hxy (Ideal.sum_mem _ fun z H => _)
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
z : ι × ι
H : z ∈ erase antidiag (max₁, max₂)
⊢ ↑(proj 𝒜 z.fst) x * ↑(proj 𝒜 z.snd) y ∈ I
[PROOFSTEP]
rcases z with ⟨i, j⟩
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H : (i, j) ∈ erase antidiag (max₁, max₂)
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
simp only [mem_erase, Prod.mk.inj_iff, Ne.def, mem_filter, mem_product] at H 
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H :
  ¬(i =
          max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
            (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
        j =
          max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
            (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))) ∧
    (i ∈ DFinsupp.support (↑(decompose 𝒜) x) ∧ j ∈ DFinsupp.support (↑(decompose 𝒜) y)) ∧
      i + j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
            (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
          max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
            (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
rcases H with ⟨H₁, ⟨H₂, H₃⟩, H₄⟩
[GOAL]
case mk.intro.intro.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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
have max_lt : max₁ < i ∨ max₂ < j :=
  by
  rcases lt_trichotomy max₁ i with (h | rfl | h)
  · exact Or.inl h
  · refine' False.elim (H₁ ⟨rfl, add_left_cancel H₄⟩)
  · apply Or.inr
    have := add_lt_add_right h j
    rw [H₄] at this 
    exact lt_of_add_lt_add_left this
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
⊢ max₁ < i ∨ max₂ < j
[PROOFSTEP]
rcases lt_trichotomy max₁ i with (h | rfl | h)
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
h : max₁ < i
⊢ max₁ < i ∨ max₂ < j
[PROOFSTEP]
exact Or.inl h
[GOAL]
case inr.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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
j : ι
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
H₁ :
  ¬(max₁ =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  max₁ + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : max₁ ∈ DFinsupp.support (↑(decompose 𝒜) x)
⊢ max₁ < max₁ ∨ max₂ < j
[PROOFSTEP]
refine' False.elim (H₁ ⟨rfl, add_left_cancel H₄⟩)
[GOAL]
case inr.inr
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
h : i < max₁
⊢ max₁ < i ∨ max₂ < j
[PROOFSTEP]
apply Or.inr
[GOAL]
case inr.inr.h
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
h : i < max₁
⊢ max₂ < j
[PROOFSTEP]
have := add_lt_add_right h j
[GOAL]
case inr.inr.h
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
h : i < max₁
this : i + j < max₁ + j
⊢ max₂ < j
[PROOFSTEP]
rw [H₄] at this 
[GOAL]
case inr.inr.h
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
h : i < max₁
this :
  max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))) <
    max₁ + j
⊢ max₂ < j
[PROOFSTEP]
exact lt_of_add_lt_add_left this
[GOAL]
case mk.intro.intro.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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
max_lt : max₁ < i ∨ max₂ < j
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
cases' max_lt with max_lt max_lt
[GOAL]
case mk.intro.intro.intro.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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
max_lt : max₁ < i
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
have not_mem : i ∉ set₁ := fun h => lt_irrefl _ ((max'_lt_iff set₁ (nonempty x rid₁)).mp max_lt i h)
[GOAL]
case mk.intro.intro.intro.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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
max_lt : max₁ < i
not_mem : ¬i ∈ set₁
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
rw [set₁_eq] at not_mem 
[GOAL]
case mk.intro.intro.intro.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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
max_lt : max₁ < i
not_mem : ¬i ∈ filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
simp only [not_and, Classical.not_not, Ne.def, mem_filter] at not_mem 
[GOAL]
case mk.intro.intro.intro.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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
max_lt : max₁ < i
not_mem : i ∈ DFinsupp.support (↑(decompose 𝒜) x) → ↑(proj 𝒜 i) x ∈ I
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
exact Ideal.mul_mem_right _ I (not_mem H₂)
[GOAL]
case mk.intro.intro.intro.inr
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
max_lt : max₂ < j
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
have not_mem : j ∉ set₂ := fun h => lt_irrefl _ ((max'_lt_iff set₂ (nonempty y rid₂)).mp max_lt j h)
[GOAL]
case mk.intro.intro.intro.inr
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
max_lt : max₂ < j
not_mem : ¬j ∈ set₂
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
rw [set₂_eq] at not_mem 
[GOAL]
case mk.intro.intro.intro.inr
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
max_lt : max₂ < j
not_mem : ¬j ∈ filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
simp only [not_and, Classical.not_not, Ne.def, mem_filter] at not_mem 
[GOAL]
case mk.intro.intro.intro.inr
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  filter (fun z => z.fst + z.snd = max₁ + max₂)
    (DFinsupp.support (↑(decompose 𝒜) x) ×ˢ DFinsupp.support (↑(decompose 𝒜) y))
ha :
  antidiag =
    filter (fun z => z.fst + z.snd = 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 in erase antidiag (max₁, max₂), ↑(proj 𝒜 ij.fst) x * ↑(proj 𝒜 ij.snd) y
i j : ι
H₁ :
  ¬(i =
        max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) ∧
      j =
        max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
          (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))))
H₄ :
  i + j =
    max' (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))) +
      max' (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y)))
        (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
H₂ : i ∈ DFinsupp.support (↑(decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support (↑(decompose 𝒜) y)
max_lt : max₂ < j
not_mem : j ∈ DFinsupp.support (↑(decompose 𝒜) y) → ↑(proj 𝒜 j) y ∈ I
⊢ ↑(proj 𝒜 (i, j).fst) x * ↑(proj 𝒜 (i, j).snd) y ∈ I
[PROOFSTEP]
exact Ideal.mul_mem_left I _ (not_mem H₃)
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
mem_I : ↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
⊢ False
[PROOFSTEP]
have not_mem_I : proj 𝒜 max₁ x * proj 𝒜 max₂ y ∉ I :=
  by
  have neither_mem : proj 𝒜 max₁ x ∉ I ∧ proj 𝒜 max₂ y ∉ I :=
    by
    rw [mem_filter] at mem_max₁ mem_max₂ 
    exact ⟨mem_max₁.2, mem_max₂.2⟩
  intro _rid
  cases' homogeneous_mem_or_mem ⟨max₁, SetLike.coe_mem _⟩ ⟨max₂, SetLike.coe_mem _⟩ mem_I with h h
  · apply neither_mem.1 h
  · apply neither_mem.2 h
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
mem_I : ↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
⊢ ¬↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
[PROOFSTEP]
have neither_mem : proj 𝒜 max₁ x ∉ I ∧ proj 𝒜 max₂ y ∉ I :=
  by
  rw [mem_filter] at mem_max₁ mem_max₂ 
  exact ⟨mem_max₁.2, mem_max₂.2⟩
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
mem_I : ↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
⊢ ¬↑(proj 𝒜 max₁) x ∈ I ∧ ¬↑(proj 𝒜 max₂) y ∈ I
[PROOFSTEP]
rw [mem_filter] at mem_max₁ mem_max₂ 
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
mem_max₁ : max₁ ∈ DFinsupp.support (↑(decompose 𝒜) x) ∧ ¬↑(proj 𝒜 max₁) x ∈ I
mem_max₂ : max₂ ∈ DFinsupp.support (↑(decompose 𝒜) y) ∧ ¬↑(proj 𝒜 max₂) y ∈ I
hxy : ↑(proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
mem_I : ↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
⊢ ¬↑(proj 𝒜 max₁) x ∈ I ∧ ¬↑(proj 𝒜 max₂) y ∈ I
[PROOFSTEP]
exact ⟨mem_max₁.2, mem_max₂.2⟩
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
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
⊢ ¬↑(proj 𝒜 max₁) x * ↑(proj 𝒜 max₂) y ∈ I
[PROOFSTEP]
intro _rid
[GOAL]
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
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
⊢ False
[PROOFSTEP]
cases' homogeneous_mem_or_mem ⟨max₁, SetLike.coe_mem _⟩ ⟨max₂, SetLike.coe_mem _⟩ mem_I with h h
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
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 :
  ↑(↑(AddMonoidHom.comp (DFinsupp.evalAddMonoidHom max₁)
            (RingHom.toAddMonoidHom (RingEquiv.toRingHom (decomposeRingEquiv 𝒜))))
        x) ∈
    I
⊢ False
[PROOFSTEP]
apply neither_mem.1 h
[GOAL]
case inr
ι : 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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
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 :
  ↑(↑(AddMonoidHom.comp (DFinsupp.evalAddMonoidHom max₂)
            (RingHom.toAddMonoidHom (RingEquiv.toRingHom (decomposeRingEquiv 𝒜))))
        y) ∈
    I
⊢ False
[PROOFSTEP]
apply neither_mem.2 h
[GOAL]
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}, Homogeneous 𝒜 x → Homogeneous 𝒜 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 : A), ¬x ∈ I → Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x)))
max₁ : ι := max' set₁ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) x ∈ I) (DFinsupp.support (↑(decompose 𝒜) x))))
max₂ : ι := max' set₂ (_ : Finset.Nonempty (filter (fun i => ¬↑(proj 𝒜 i) y ∈ I) (DFinsupp.support (↑(decompose 𝒜) y))))
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
[PROOFSTEP]
exact not_mem_I mem_I
[GOAL]
ι : 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 : IsPrime I
⊢ IsPrime (HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I))
[PROOFSTEP]
apply (Ideal.homogeneousCore 𝒜 I).is_homogeneous'.isPrime_of_homogeneous_mem_or_mem
[GOAL]
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 : IsPrime I
⊢ (Ideal.homogeneousCore 𝒜 I).toSubmodule ≠ ⊤
[PROOFSTEP]
exact ne_top_of_le_ne_top h.ne_top (Ideal.toIdeal_homogeneousCore_le 𝒜 I)
[GOAL]
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 : IsPrime I
⊢ ∀ {x y : A},
    Homogeneous 𝒜 x →
      Homogeneous 𝒜 y →
        x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule →
          x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
[PROOFSTEP]
rintro x y hx hy hxy
[GOAL]
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 : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
[PROOFSTEP]
have H := h.mem_or_mem (Ideal.toIdeal_homogeneousCore_le 𝒜 I hxy)
[GOAL]
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 : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
H : x ∈ I ∨ y ∈ I
⊢ x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
[PROOFSTEP]
refine' H.imp _ _
[GOAL]
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 : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
H : x ∈ I ∨ y ∈ I
⊢ x ∈ I → x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
[PROOFSTEP]
exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hx
[GOAL]
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 : IsPrime I
x y : A
hx : Homogeneous 𝒜 x
hy : Homogeneous 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
[PROOFSTEP]
exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hy
[GOAL]
ι : 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
⊢ radical I = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
[PROOFSTEP]
rw [Ideal.radical_eq_sInf]
[GOAL]
ι : 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 ∧ IsPrime J} = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
[PROOFSTEP]
apply le_antisymm
[GOAL]
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 ∧ IsPrime J} ≤ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
[PROOFSTEP]
exact sInf_le_sInf fun J => And.right
[GOAL]
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 ∧ IsPrime J} ≤ InfSet.sInf {J | I ≤ J ∧ IsPrime J}
[PROOFSTEP]
refine sInf_le_sInf_of_forall_exists_le ?_
[GOAL]
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 : Ideal A), x ∈ {J | I ≤ J ∧ IsPrime J} → ∃ y, y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J} ∧ y ≤ x
[PROOFSTEP]
rintro J ⟨HJ₁, HJ₂⟩
[GOAL]
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₂ : IsPrime J
⊢ ∃ y, y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J} ∧ y ≤ J
[PROOFSTEP]
refine ⟨(J.homogeneousCore 𝒜).toIdeal, ?_, J.toIdeal_homogeneousCore_le _⟩
[GOAL]
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₂ : IsPrime J
⊢ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J) ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
[PROOFSTEP]
refine ⟨HomogeneousIdeal.isHomogeneous _, ?_, HJ₂.homogeneousCore⟩
[GOAL]
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₂ : IsPrime J
⊢ I ≤ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J)
[PROOFSTEP]
exact hI.toIdeal_homogeneousCore_eq_self.symm.trans_le (Ideal.homogeneousCore_mono _ HJ₁)
[GOAL]
ι : 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 : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (Ideal.radical I)
[PROOFSTEP]
rw [h.radical_eq]
[GOAL]
ι : 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 : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J})
[PROOFSTEP]
exact Ideal.IsHomogeneous.sInf fun _ => And.left
