awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (hypothesis)
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
hxy : x * y ∈ I
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}
⊢ False
have set₂_eq : let set₂ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I};
set₂ =
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y) |
    ((proj 𝒜 i : (a : A) → A) y : A) ∉ I}
Tactic: set set₂ := {i ∈ (decompose 𝒜 y).support | proj 𝒜 i y ∉ I} with set₂_eq
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
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_1 y : A
hxy : x_1 * y ∈ I
rid₁ : x_1 ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1) |
    ((proj 𝒜 i : (a : A) → A) x_1 : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1) |
      ((proj 𝒜 i : (a : A) → A) x_1 : 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}
x : A
hx : 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})
have rw : ∃ (a : ι),
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) a ∧
    ((proj 𝒜 a : (a : A) → A) x : A) ∉ I
Tactic: rw [filter_nonempty_iff]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
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_1 y : A
hxy : x_1 * y ∈ I
rid₁ : x_1 ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1) |
    ((proj 𝒜 i : (a : A) → A) x_1 : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1) |
      ((proj 𝒜 i : (a : A) → A) x_1 : 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}
x : A
hx : x ∉ I
⊢ ∃ (a : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) a ∧
      ((proj 𝒜 a : (a : A) → A) x : A) ∉ I
have contrapose! : ∀
  (hx :
    ∀ (a : ι)
      (_ :
        Membership.mem (γ := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) a),
      Membership.mem (α := A) I ((proj 𝒜 a : (a : A) → A) x : A)),
  x ∈ I
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
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_1 y : A
hxy : x_1 * y ∈ I
rid₁ : x_1 ∉ I
rid₂ : y ∉ I
set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1) |
    ((proj 𝒜 i : (a : A) → A) x_1 : A) ∉ I}
set₁_eq :
  set₁ =
    {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1) |
      ((proj 𝒜 i : (a : A) → A) x_1 : 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}
x : A
hx :
  ∀ (a : ι)
    (_ :
      Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) a),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) a) : A) ∈ I
⊢ x ∈ I
have rw : ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈
  I
Tactic: rw [← sum_support_decompose 𝒜 x]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (hypothesis)
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
hxy : x * y ∈ I
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}
⊢ False
have 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})
Tactic: have nonempty :
        ∀ x : A, x ∉ I → {i ∈ (decompose 𝒜 x).support | 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
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (hypothesis)
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
hxy : x * y ∈ I
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' ⋯
⊢ False
have mem_max₁ : max₁ ∈ set₁
Tactic: have mem_max₁ : max₁ ∈ set₁ := max'_mem set₁ (nonempty x rid₁)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (hypothesis)
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
hxy : x * y ∈ I
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₁
⊢ False
have mem_max₂ : max₂ ∈ set₂
Tactic: have mem_max₂ : max₂ ∈ set₂ := max'_mem set₂ (nonempty y rid₂)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (hypothesis)
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
hxy : x * y ∈ I
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₂
⊢ False
have hxy₁ : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
Tactic: replace hxy : proj 𝒜 (max₁ + max₂) (x * y) ∈ I := hI _ hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (hypothesis)
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)
⊢ HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
have ha : let 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₂};
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₂}
Tactic: set antidiag :=
          {z ∈ (decompose 𝒜 x).support ×ˢ (decompose 𝒜 y).support | z.1 + z.2 = max₁ + max₂}
           with ha
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
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₂}
⊢ (max₁, max₂) ∈ antidiag
have simp : (Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) max₁ ∧
    Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) max₂) ∧
  True
Tactic: simp only [antidiag, mem_filter, mem_product]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (hypothesis)
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₂}
⊢ HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
have mem_antidiag : (max₁, max₂) ∈ antidiag
Tactic: have mem_antidiag : (max₁, max₂) ∈ antidiag := by
          simp only [antidiag, mem_filter, mem_product]
          exact ⟨⟨mem_of_mem_filter _ mem_max₁, mem_of_mem_filter _ mem_max₂⟩, trivial⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (hypothesis)
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
⊢ HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
have 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)
Tactic: have eq_add_sum :=
          calc
            proj 𝒜 (max₁ + max₂) (x * y) = ∑ ij ∈ 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 ∈ antidiag.erase (max₁, max₂), proj 𝒜 ij.1 x * proj 𝒜 ij.2 y :=
              (add_sum_erase _ _ mem_antidiag).symm