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)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
mem_max₃ :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) max₁ ∧
    ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I
mem_max₄ :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) max₂ ∧
    ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I
⊢ Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)

Tactic:
rw [mem_filter] at mem_max₁ mem_max₂

Premises used: Finset.mem_filter
-- 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)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
mem_max₃ :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) max₁ ∧
    ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I
mem_max₄ :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) max₂ ∧
    ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I
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

Tactic:
rw [mem_filter] at mem_max₁ mem_max₂

Premises used: Finset.mem_filter
-- 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₁ :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) max₁ ∧
    ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I
mem_max₂ :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) max₂ ∧
    ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
⊢ ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I ∧ ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I

Tactic:
⟨mem_max₁.2, mem_max₂.2⟩

Premises used: And.right, And.intro
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
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₁ :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) max₁ ∧
    ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I
mem_max₂ :
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) max₂ ∧
    ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I
hxy : Membership.mem (α := A) I ((proj 𝒜 (max₁ + max₂) : (a : A) → A) (x * y) : A)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
⊢ ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I ∧ ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I

Tactic:
exact ⟨mem_max₁.2, mem_max₂.2⟩
-- 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)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
⊢ ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I ∧ ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I

Tactic:
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⟩
-- 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)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
neither_mem : ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I ∧ ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I
_rid : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
inl :
  ∀
    (h :
      (↑(((AddMonoidHom.comp (N := Π₀ (i : ι), ↥(𝒜 i))
                    (DFinsupp.evalAddMonoidHom (β := fun (i : ι) ↦ ↥(𝒜 i)) max₁ : (Π₀ (i : ι), ↥(𝒜 i)) →+ ↥(𝒜 max₁))
                    (RingHom.toAddMonoidHom (RingEquiv.toRingHom (decomposeRingEquiv 𝒜)) : A →+ ⨁ (i : ι), ↥(𝒜 i)) :
                  A →+ ↥(𝒜 max₁)) :
                (a : A) → ↥(𝒜 max₁))
              x) :
          A) ∈
        I),
    False
inr :
  ∀
    (h :
      (↑(((AddMonoidHom.comp (N := Π₀ (i : ι), ↥(𝒜 i))
                    (DFinsupp.evalAddMonoidHom (β := fun (i : ι) ↦ ↥(𝒜 i)) max₂ : (Π₀ (i : ι), ↥(𝒜 i)) →+ ↥(𝒜 max₂))
                    (RingHom.toAddMonoidHom (RingEquiv.toRingHom (decomposeRingEquiv 𝒜)) : A →+ ⨁ (i : ι), ↥(𝒜 i)) :
                  A →+ ↥(𝒜 max₂)) :
                (a : A) → ↥(𝒜 max₂))
              y) :
          A) ∈
        I),
    False
⊢ False

Tactic:
rcases homogeneous_mem_or_mem ⟨max₁, SetLike.coe_mem _⟩ ⟨max₂, SetLike.coe_mem _⟩ mem_I
          with h | h

Premises used: SetLike.coe_mem, Exists.intro
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
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)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
neither_mem : ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I ∧ ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I
_rid : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
h :
  (↑(((AddMonoidHom.comp (N := Π₀ (i : ι), ↥(𝒜 i))
                (DFinsupp.evalAddMonoidHom (β := fun (i : ι) ↦ ↥(𝒜 i)) max₁ : (Π₀ (i : ι), ↥(𝒜 i)) →+ ↥(𝒜 max₁))
                (RingHom.toAddMonoidHom (RingEquiv.toRingHom (decomposeRingEquiv 𝒜)) : A →+ ⨁ (i : ι), ↥(𝒜 i)) :
              A →+ ↥(𝒜 max₁)) :
            (a : A) → ↥(𝒜 max₁))
          x) :
      A) ∈
    I
⊢ False

Tactic:
apply neither_mem.1 h

Premises used: And.left
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
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)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
neither_mem : ((proj 𝒜 max₁ : (a : A) → A) x : A) ∉ I ∧ ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I
_rid : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
h :
  (↑(((AddMonoidHom.comp (N := Π₀ (i : ι), ↥(𝒜 i))
                (DFinsupp.evalAddMonoidHom (β := fun (i : ι) ↦ ↥(𝒜 i)) max₂ : (Π₀ (i : ι), ↥(𝒜 i)) →+ ↥(𝒜 max₂))
                (RingHom.toAddMonoidHom (RingEquiv.toRingHom (decomposeRingEquiv 𝒜)) : A →+ ⨁ (i : ι), ↥(𝒜 i)) :
              A →+ ↥(𝒜 max₂)) :
            (a : A) → ↥(𝒜 max₂))
          y) :
      A) ∈
    I
⊢ False

Tactic:
apply neither_mem.2 h

Premises used: And.right
-- Module: Mathlib.RingTheory.GradedAlgebra.Radical
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
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)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
⊢ HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I

Tactic:
have notMem_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
        rcases 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
-- 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)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
notMem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I
⊢ False

Tactic:
notMem_I mem_I
-- 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)
mem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∈ I
notMem_I : HMul.hMul (α := A) (β := A) ((proj 𝒜 max₁ : (a : A) → A) x : A) ((proj 𝒜 max₂ : (a : A) → A) y : A) ∉ I
⊢ False

Tactic:
exact notMem_I mem_I