awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
      ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₂ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
set₂_eq :
  set₂ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
      ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
nonempty :
  ∀ x ∉ I,
    Finset.Nonempty.{u_1} (α := ι)
      ({i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
        ((proj 𝒜 i : (a : A) → A) x : A) ∉ I})
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
antidiag : Finset (ι × ι) :=
  {z ∈
      SProd.sprod (α := Finset ι) (β := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
    z.1 + z.2 = max₁ + max₂}
ha :
  antidiag =
    {z ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
      z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) +
      ∑ ij ∈ antidiag.erase (max₁, max₂),
        HMul.hMul (α := A) (β := A) ((proj 𝒜 ij.1 : (a : A) → A) x : A) ((proj 𝒜 ij.2 : (a : A) → A) y : A)
z : ι × ι
H : z ∈ antidiag.erase (max₁, max₂)
rcases :
  ∀ (i j : ι) (H : (i, j) ∈ antidiag.erase (max₁, max₂)),
    HMul.hMul (α := A) (β := A) ((proj 𝒜 (i, j).1 : (a : A) → A) x : A) ((proj 𝒜 (i, j).2 : (a : A) → A) y : A) ∈ I
⊢ HMul.hMul (α := A) (β := A) ((proj 𝒜 z.1 : (a : A) → A) x : A) ((proj 𝒜 z.2 : (a : A) → A) y : A) ∈ I

Tactic:
rcases z with ⟨i, j⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
      ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₂ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
set₂_eq :
  set₂ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
      ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
nonempty :
  ∀ x ∉ I,
    Finset.Nonempty.{u_1} (α := ι)
      ({i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
        ((proj 𝒜 i : (a : A) → A) x : A) ∉ I})
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
antidiag : Finset (ι × ι) :=
  {z ∈
      SProd.sprod (α := Finset ι) (β := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
    z.1 + z.2 = max₁ + max₂}
ha :
  antidiag =
    {z ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
      z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) +
      ∑ ij ∈ antidiag.erase (max₁, max₂),
        HMul.hMul (α := A) (β := A) ((proj 𝒜 ij.1 : (a : A) → A) x : A) ((proj 𝒜 ij.2 : (a : A) → A) y : A)
i j : ι
H : (i, j) ∈ antidiag.erase (max₁, max₂)
⊢ ¬(i = max₁ ∧ j = max₂) ∧
    (Membership.mem (γ := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) i ∧
        Membership.mem (γ := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) j) ∧
      i + j = max₁ + max₂

Tactic:
simp only [antidiag, mem_erase, Prod.mk_inj, Ne, mem_filter, mem_product] at H

Premises used: Prod.mk_inj, Ne, Finset.mem_erase, Finset.mem_filter, Finset.mem_product
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
      ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₂ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
set₂_eq :
  set₂ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
      ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
nonempty :
  ∀ x ∉ I,
    Finset.Nonempty.{u_1} (α := ι)
      ({i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
        ((proj 𝒜 i : (a : A) → A) x : A) ∉ I})
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
antidiag : Finset (ι × ι) :=
  {z ∈
      SProd.sprod (α := Finset ι) (β := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
    z.1 + z.2 = max₁ + max₂}
ha :
  antidiag =
    {z ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
      z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) +
      ∑ ij ∈ antidiag.erase (max₁, max₂),
        HMul.hMul (α := A) (β := A) ((proj 𝒜 ij.1 : (a : A) → A) x : A) ((proj 𝒜 ij.2 : (a : A) → A) y : A)
i j : ι
H :
  ¬(i = max₁ ∧ j = max₂) ∧
    (Membership.mem (γ := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) i ∧
        Membership.mem (γ := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) j) ∧
      i + j = max₁ + max₂
⊢ ¬(i = max₁ ∧ j = max₂)

Tactic:
rcases H with ⟨H₁, ⟨H₂, H₃⟩, H₄⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
      ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₂ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
set₂_eq :
  set₂ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
      ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
nonempty :
  ∀ x ∉ I,
    Finset.Nonempty.{u_1} (α := ι)
      ({i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
        ((proj 𝒜 i : (a : A) → A) x : A) ∉ I})
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
antidiag : Finset (ι × ι) :=
  {z ∈
      SProd.sprod (α := Finset ι) (β := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
    z.1 + z.2 = max₁ + max₂}
ha :
  antidiag =
    {z ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
      z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) +
      ∑ ij ∈ antidiag.erase (max₁, max₂),
        HMul.hMul (α := A) (β := A) ((proj 𝒜 ij.1 : (a : A) → A) x : A) ((proj 𝒜 ij.2 : (a : A) → A) y : A)
i j : ι
H :
  ¬(i = max₁ ∧ j = max₂) ∧
    (Membership.mem (γ := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) i ∧
        Membership.mem (γ := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) j) ∧
      i + j = max₁ + max₂
H₁ : ¬(i = max₁ ∧ j = max₂)
⊢ i + j = max₁ + max₂

Tactic:
rcases H with ⟨H₁, ⟨H₂, H₃⟩, H₄⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
      ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₂ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
set₂_eq :
  set₂ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
      ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
nonempty :
  ∀ x ∉ I,
    Finset.Nonempty.{u_1} (α := ι)
      ({i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
        ((proj 𝒜 i : (a : A) → A) x : A) ∉ I})
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
antidiag : Finset (ι × ι) :=
  {z ∈
      SProd.sprod (α := Finset ι) (β := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
    z.1 + z.2 = max₁ + max₂}
ha :
  antidiag =
    {z ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
      z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) +
      ∑ ij ∈ antidiag.erase (max₁, max₂),
        HMul.hMul (α := A) (β := A) ((proj 𝒜 ij.1 : (a : A) → A) x : A) ((proj 𝒜 ij.2 : (a : A) → A) y : A)
i j : ι
H :
  ¬(i = max₁ ∧ j = max₂) ∧
    (Membership.mem (γ := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) i ∧
        Membership.mem (γ := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) j) ∧
      i + j = max₁ + max₂
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
⊢ Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) i

Tactic:
rcases H with ⟨H₁, ⟨H₂, H₃⟩, H₄⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
      ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₂ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
set₂_eq :
  set₂ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
      ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
nonempty :
  ∀ x ∉ I,
    Finset.Nonempty.{u_1} (α := ι)
      ({i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
        ((proj 𝒜 i : (a : A) → A) x : A) ∉ I})
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
antidiag : Finset (ι × ι) :=
  {z ∈
      SProd.sprod (α := Finset ι) (β := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
    z.1 + z.2 = max₁ + max₂}
ha :
  antidiag =
    {z ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
      z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) +
      ∑ ij ∈ antidiag.erase (max₁, max₂),
        HMul.hMul (α := A) (β := A) ((proj 𝒜 ij.1 : (a : A) → A) x : A) ((proj 𝒜 ij.2 : (a : A) → A) y : A)
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) i
H₃ :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) j
⊢ max₁ ≤ i ∨ max₂ < j

Tactic:
le_or_lt_of_add_le_add H₄.ge

Premises used: Eq.ge, le_or_lt_of_add_le_add
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
      ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₂ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
set₂_eq :
  set₂ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
      ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
nonempty :
  ∀ x ∉ I,
    Finset.Nonempty.{u_1} (α := ι)
      ({i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
        ((proj 𝒜 i : (a : A) → A) x : A) ∉ I})
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
antidiag : Finset (ι × ι) :=
  {z ∈
      SProd.sprod (α := Finset ι) (β := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
    z.1 + z.2 = max₁ + max₂}
ha :
  antidiag =
    {z ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
      z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) +
      ∑ ij ∈ antidiag.erase (max₁, max₂),
        HMul.hMul (α := A) (β := A) ((proj 𝒜 ij.1 : (a : A) → A) x : A) ((proj 𝒜 ij.2 : (a : A) → A) y : A)
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) i
H₃ :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) j
h : max₁ < i ↔ max₁ ≤ i
⊢ max₁ < i ∨ max₂ < j

Tactic:
convert! le_or_lt_of_add_le_add H₄.ge using 1

Premises used: Eq.ge, le_or_lt_of_add_le_add
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
      ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
set₂ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
set₂_eq :
  set₂ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
      ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
nonempty :
  ∀ x ∉ I,
    Finset.Nonempty.{u_1} (α := ι)
      ({i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
        ((proj 𝒜 i : (a : A) → A) x : A) ∉ I})
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
antidiag : Finset (ι × ι) :=
  {z ∈
      SProd.sprod (α := Finset ι) (β := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
    z.1 + z.2 = max₁ + max₂}
ha :
  antidiag =
    {z ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) |
      z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) +
      ∑ ij ∈ antidiag.erase (max₁, max₂),
        HMul.hMul (α := A) (β := A) ((proj 𝒜 ij.1 : (a : A) → A) x : A) ((proj 𝒜 ij.2 : (a : A) → A) y : A)
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) i
H₃ :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) j
h : max₁ ≠ i
⊢ max₁ < i ↔ max₁ ≤ i

Tactic:
rw [Ne.le_iff_lt]

Premises used: Ne.le_iff_lt