awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
a : R
rw : IsRegular a ↔ Membership.mem (γ := Submonoid R) R⁰ a
rw₁ rw₂ : Membership.mem (γ := Submonoid R) R⁰ a ↔ Membership.mem (γ := Submonoid R) R⁰ a
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid R) R⁰ a

Tactic:
rw [isUnit_iff_isRegular, isRegular_iff_mem_nonZeroDivisors]

Premises used: isRegular_iff_mem_nonZeroDivisors, IsArtinianRing.isUnit_iff_isRegular
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
a : R
rw : IsRegular a ↔ Membership.mem (γ := Submonoid R) R⁰ a
rw₁ rw₂ : Membership.mem (γ := Submonoid R) R⁰ a ↔ Membership.mem (γ := Submonoid R) R⁰ a
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid R) R⁰ a

Tactic:
rw [isUnit_iff_isRegular_of_mulOpposite, isRegular_iff_mem_nonZeroDivisors]

Premises used: IsArtinianRing.isUnit_iff_isRegular_of_mulOpposite, isRegular_iff_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
h :
  ∀ (x : R),
    Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x
⊢ Eq (α := Submonoid R) (IsUnit.submonoid R : Submonoid R) (R⁰ : Submonoid R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
x : R
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x

Tactic:
simp [IsUnit.mem_submonoid_iff, isUnit_iff_mem_nonZeroDivisors]

Premises used: IsArtinianRing.isUnit_iff_mem_nonZeroDivisors, IsUnit.mem_submonoid_iff
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
h :
  ∀ (x : R),
    Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x
⊢ Eq (α := Submonoid R) (IsUnit.submonoid R : Submonoid R) (R⁰ : Submonoid R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x

Tactic:
simp [IsUnit.mem_submonoid_iff, isUnit_iff_mem_nonZeroDivisors_of_mulOpposite]

Premises used: IsUnit.mem_submonoid_iff, IsArtinianRing.isUnit_iff_mem_nonZeroDivisors_of_mulOpposite
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
h :
  ∀ (x : R),
    Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔
      Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R : Submonoid R) x
⊢ Eq (α := Submonoid R) (IsUnit.submonoid R : Submonoid R) (nonZeroDivisorsRight R : Submonoid R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
x : R
h : Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ IsRightRegular x
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R : Submonoid R) x

Tactic:
rw [← isRightRegular_iff_mem_nonZeroDivisorsRight]

Premises used: isRightRegular_iff_mem_nonZeroDivisorsRight
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
x : R
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ IsRightRegular x

Tactic:
isUnit_iff_isRightRegular

Premises used: Set.Mem, setOf, IsUnit, IsArtinianRing.isUnit_iff_isRightRegular
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
x : R
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ IsRightRegular x

Tactic:
exact isUnit_iff_isRightRegular

Premises used: IsArtinianRing.isUnit_iff_isRightRegular
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
h :
  ∀ (x : R),
    Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔
      Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R : Submonoid R) x
⊢ Eq (α := Submonoid R) (IsUnit.submonoid R : Submonoid R) (nonZeroDivisorsLeft R : Submonoid R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
h : Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ IsLeftRegular x
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R : Submonoid R) x

Tactic:
rw [← isLeftRegular_iff_mem_nonZeroDivisorsLeft]

Premises used: isLeftRegular_iff_mem_nonZeroDivisorsLeft
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ IsLeftRegular x

Tactic:
isUnit_iff_isLeftRegular

Premises used: Set.Mem, setOf, IsUnit, IsArtinianRing.isUnit_iff_isLeftRegular
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
⊢ Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x ↔ IsLeftRegular x

Tactic:
exact isUnit_iff_isLeftRegular

Premises used: IsArtinianRing.isUnit_iff_isLeftRegular
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
have :
  ∀ (s : Finset { I : Ideal R // I.IsMaximal })
    (H :
      ∀ (a : { I : Ideal R // I.IsMaximal }),
        s.inf (Subtype.val (p := fun (I : Ideal R) ↦ I.IsMaximal)) ≤ (↑a : Ideal R)),
    Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}

Tactic:
have ⟨s, H⟩ := Finset.exists_inf_le (Subtype.val (p := fun I : Ideal R ↦ I.IsMaximal))
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
s : Finset { I : Ideal R // I.IsMaximal }
H : ∀ (a : { I : Ideal R // I.IsMaximal }), s.inf (Subtype.val (p := fun (I : Ideal R) ↦ I.IsMaximal)) ≤ (↑a : Ideal R)
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}

Tactic:
Set.finite_def.2 ⟨s, fun p ↦ ?_⟩

Premises used: Iff.mpr, Nonempty.intro, Fintype.mk, Set.finite_def
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
s : Finset { I : Ideal R // I.IsMaximal }
H : ∀ (a : { I : Ideal R // I.IsMaximal }), s.inf (Subtype.val (p := fun (I : Ideal R) ↦ I.IsMaximal)) ≤ (↑a : Ideal R)
refine : ∀ (p : (↑{I : Ideal R | I.IsMaximal} : Type u_1)), p ∈ s
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}

Tactic:
refine Set.finite_def.2 ⟨s, fun p ↦ ?_⟩

Premises used: Iff.mpr, Nonempty.intro, Fintype.mk, Set.finite_def
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
s : Finset { I : Ideal R // I.IsMaximal }
H : ∀ (a : { I : Ideal R // I.IsMaximal }), s.inf (Subtype.val (p := fun (I : Ideal R) ↦ I.IsMaximal)) ≤ (↑a : Ideal R)
p : (↑{I : Ideal R | I.IsMaximal} : Type u_1)
have : ∀ (q : { I : Ideal R // I.IsMaximal }) (hq1 : q ∈ s) (hq2 : (↑q : Ideal R) ≤ (↑p : Ideal R)), p ∈ s
⊢ p ∈ s

Tactic:
have ⟨q, hq1, hq2⟩ := p.2.isPrime.inf_le'.mp (H p)
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
s : Finset { I : Ideal R // I.IsMaximal }
H : ∀ (a : { I : Ideal R // I.IsMaximal }), s.inf (Subtype.val (p := fun (I : Ideal R) ↦ I.IsMaximal)) ≤ (↑a : Ideal R)
p : (↑{I : Ideal R | I.IsMaximal} : Type u_1)
q : { I : Ideal R // I.IsMaximal }
hq1 : q ∈ s
hq2 : (↑q : Ideal R) ≤ (↑p : Ideal R)
rwa rwa₁ rwa₂ rwa₃ : q ∈ s
⊢ p ∈ s

Tactic:
rwa [← Subtype.ext <| q.2.eq_of_le p.2.ne_top hq2]

Premises used: Ideal.IsMaximal.eq_of_le, Ideal.IsMaximal.ne_top, Subtype.property, Subtype.ext
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsArtinianRing R
⊢ Finite.{u_1 + 1} (MaximalSpectrum R)

Tactic:
haveI : Finite {I : Ideal R // I.IsMaximal} := (setOf_isMaximal_finite R).to_subtype
  .of_equiv _ (MaximalSpectrum.equivSubtype _).symm

Premises used: Finite.of_equiv, Subtype, MaximalSpectrum.equivSubtype, Ideal.IsMaximal, Equiv.symm
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
⊢ IsField R

Tactic:
⟨Nontrivial.exists_pair_ne, mul_comm, fun {x} hx ↦ ?_⟩

Premises used: mul_comm, IsField.mk, Nontrivial.exists_pair_ne
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
refine : ∀ {x : R} (hx : x ≠ 0), ∃ (b : R), x * b = 1
⊢ IsField R

Tactic:
refine ⟨Nontrivial.exists_pair_ne, mul_comm, fun {x} hx ↦ ?_⟩
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
obtain : ∀ (n : ℕ) (y : R) (hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1), ∃ (b : R), x * b = 1
⊢ ∃ (b : R), x * b = 1

Tactic:
obtain ⟨n, y, hy⟩ := IsArtinian.exists_pow_succ_smul_dvd x (1 : R)

Premises used: IsArtinian.exists_pow_succ_smul_dvd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1
rw : x ^ n * (x * y) = x ^ n * 1
⊢ x ^ n * (x * y - 1) = 0

Tactic:
rw [mul_sub, sub_eq_zero]

Premises used: mul_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1
⊢ x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1

Tactic:
hy
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1
h : x ^ n * (x * y) = x ^ n.succ • y
⊢ x ^ n * (x * y) = x ^ n * 1

Tactic:
convert! hy using 1
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1
⊢ x ^ n * (x * y) = x ^ n.succ • y

Tactic:
simp [Nat.succ_eq_add_one, pow_add, mul_assoc]

Premises used: Nat.succ_eq_add_one, mul_assoc, pow_add
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = HSMul.hSMul (β := R) (x ^ n) 1
⊢ x ^ n * (x * y - 1) = 0

Tactic:
replace hy : x ^ n * (x * y - 1) = 0 := by
    rw [mul_sub, sub_eq_zero]
    convert! hy using 1
    simp [Nat.succ_eq_add_one, pow_add, mul_assoc]
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n * (x * y - 1) = 0
⊢ x ^ n = 0 ∨ x * y = 1

Tactic:
rw [mul_eq_zero, sub_eq_zero] at hy

Premises used: sub_eq_zero, mul_eq_zero
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n = 0 ∨ x * y = 1
⊢ ∃ (b : R), x * b = 1

Tactic:
⟨_, hy.resolve_left <| pow_ne_zero _ hx⟩

Premises used: pow_ne_zero, Or.resolve_left, Exists.intro
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n = 0 ∨ x * y = 1
⊢ ∃ (b : R), x * b = 1

Tactic:
exact ⟨_, hy.resolve_left <| pow_ne_zero _ hx⟩
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : IsArtinianRing R_1
R : Type u_2
inst_2 : CommRing R
p : Ideal R
inst_3 : p.IsPrime
inst_4 : IsArtinianRing R
⊢ p.IsMaximal

Tactic:
Ideal.Quotient.maximal_of_isField _ (isField_of_isDomain _)

Premises used: IsArtinianRing.isField_of_isDomain, Ideal.Quotient.maximal_of_isField
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
⊢ p.IsPrime ↔ p.IsMaximal

Tactic:
⟨fun _ ↦ isMaximal_of_isPrime p, fun h ↦ h.isPrime⟩

Premises used: Ideal.IsMaximal.isPrime, IsArtinianRing.isMaximal_of_isPrime, Iff.intro
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
I p : Ideal R
hp : p.IsPrime
hIp : I ≤ p
⊢ p ∈ I.minimalPrimes

Tactic:
⟨⟨hp, hIp⟩, fun q ⟨_, _⟩ hqp ↦ ((isMaximal_of_isPrime q).eq_of_le hp.ne_top hqp).ge⟩

Premises used: Eq.ge, Set.Mem, setOf, LE.le, IsArtinianRing.isMaximal_of_isPrime, Ideal.IsMaximal.eq_of_le, Ideal.IsMinimalPrime, And.intro, _private.0.IsArtinianRing.mem_minimalPrimes.match_1, Ideal.IsPrime.ne_top, Minimal
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ Eq.{u_1 + 1} (α := PrimeSpectrum R → Ideal R)
    (MaximalSpectrum.asIdeal ∘ (⇑primeSpectrumEquivMaximalSpectrum : (a : PrimeSpectrum R) → MaximalSpectrum R))
    PrimeSpectrum.asIdeal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ Eq.{u_1 + 1} (α := MaximalSpectrum R → Ideal R)
    (PrimeSpectrum.asIdeal ∘
      (⇑(Equiv.symm primeSpectrumEquivMaximalSpectrum) : (a : MaximalSpectrum R) → PrimeSpectrum R))
    MaximalSpectrum.asIdeal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) (range PrimeSpectrum.asIdeal) (range MaximalSpectrum.asIdeal)

Tactic:
simp only [PrimeSpectrum.range_asIdeal, MaximalSpectrum.range_asIdeal,
    isPrime_iff_isMaximal]

Premises used: MaximalSpectrum.range_asIdeal, IsArtinianRing.isPrime_iff_isMaximal, PrimeSpectrum.range_asIdeal
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
n : ℕ
have :
  ∀ (this : Fintype (MaximalSpectrum R)),
    HPow.hPow (α := Ideal R) (nilradical R) n = ⨅ (I : MaximalSpectrum R), I.asIdeal ^ n
⊢ HPow.hPow (α := Ideal R) (nilradical R) n = ⨅ (I : MaximalSpectrum R), I.asIdeal ^ n

Tactic:
have : Fintype (MaximalSpectrum R) := Fintype.ofFinite (MaximalSpectrum R)
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
n : ℕ
this : Fintype (MaximalSpectrum R)
rw :
  HPow.hPow (α := Ideal R) (iInf PrimeSpectrum.asIdeal) n =
    ⨅ x ∈ (↑Finset.univ : Set (MaximalSpectrum R)), x.asIdeal ^ n
⊢ HPow.hPow (α := Ideal R) (nilradical R) n = ⨅ (I : MaximalSpectrum R), I.asIdeal ^ n

Tactic:
rw [← iInf_univ, ← Finset.coe_univ, PrimeSpectrum.nilradical_eq_iInf]

Premises used: Finset.coe_univ, PrimeSpectrum.nilradical_eq_iInf, iInf_univ
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
n : ℕ
this : Fintype (MaximalSpectrum R)
rw :
  HPow.hPow (α := Ideal R) (iInf PrimeSpectrum.asIdeal) n =
    HPow.hPow (α := Ideal R)
      (⨅ (i : MaximalSpectrum R), ⨅ (_ : Membership.mem (γ := Finset (MaximalSpectrum R)) Finset.univ i), i.asIdeal) n
⊢ HPow.hPow (α := Ideal R) (iInf PrimeSpectrum.asIdeal) n =
    ⨅ (x : MaximalSpectrum R), ⨅ (_ : Membership.mem (γ := Finset (MaximalSpectrum R)) Finset.univ x), x.asIdeal ^ n

Tactic:
rw [← Ideal.prod_eq_iInf_of_pairwise_isCoprime fun I _ _ _ ↦ .pow ∘ I.isCoprime_of_ne,
    Finset.prod_pow, Ideal.prod_eq_iInf_of_pairwise_isCoprime fun I _ _ _ ↦ I.isCoprime_of_ne]

Premises used: Function.comp, IsCoprime.pow, Ideal.prod_eq_iInf_of_pairwise_isCoprime, Finset.prod_pow
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
n : ℕ
this : Fintype (MaximalSpectrum R)
⊢ HPow.hPow (α := Ideal R) (iInf PrimeSpectrum.asIdeal) n =
    HPow.hPow (α := Ideal R)
      (⨅ (i : MaximalSpectrum R), ⨅ (_ : Membership.mem (γ := Finset (MaximalSpectrum R)) Finset.univ i), i.asIdeal) n

Tactic:
simp [Finset.mem_univ, iInf, IsArtinianRing.primeSpectrum_asIdeal_range_eq]

Premises used: Finset.mem_univ, iInf, IsArtinianRing.primeSpectrum_asIdeal_range_eq
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ Eq (α := Ideal R) (nilradical R) (iInf MaximalSpectrum.asIdeal)

Tactic:
simpa using nilradical_pow_eq_iInf R 1

Premises used: IsArtinianRing.nilradical_pow_eq_iInf, OfNat.ofNat
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsPrime}

Tactic:
simpa only [isPrime_iff_isMaximal] using setOf_isMaximal_finite R

Premises used: IsArtinianRing.isPrime_iff_isMaximal, IsArtinianRing.setOf_isMaximal_finite
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ Finite.{u_1 + 1} (PrimeSpectrum R)

Tactic:
haveI : Finite {I : Ideal R // I.IsPrime} := (setOf_isPrime_finite R).to_subtype
  .of_equiv _ (PrimeSpectrum.equivSubtype _).symm.toEquiv

Premises used: Finite.of_equiv, PrimeSpectrum.equivSubtype, Subtype, OrderIso.symm, Ideal.IsPrime, RelIso.toEquiv
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsReduced R
⊢ IsSemisimpleRing R

Tactic:
(equivPi R).symm.isSemisimpleRing

Premises used: AlgEquiv.symm, IsArtinianRing.equivPi, AlgEquiv.toRingEquiv, RingEquiv.isSemisimpleRing
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
⊢ IsSemisimpleRing R ↔ Eq (α := Ideal R) (Ring.jacobson R) ⊥

Tactic:
IsArtinian.isSemisimpleModule_iff_jacobson R R

Premises used: IsArtinian.isSemisimpleModule_iff_jacobson
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
have :
  ∀ (n : ℕ)
    (hn :
      ∀ (m : ℕ),
        n ≤ m →
          Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
            (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
            (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)),
    IsNilpotent (R := Ideal R) (Ring.jacobson R)
⊢ IsNilpotent (R := Ideal R) (Ring.jacobson R)

Tactic:
have ⟨n, hn⟩ := IsArtinian.monotone_stabilizes ⟨(Jac ^ ·), @Ideal.pow_le_pow_right _ _ _⟩
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
rw : Jac ^ (n + 1) = Jac ^ n
⊢ Jac * Jac ^ n = Jac ^ n

Tactic:
rw [← Ideal.IsTwoSided.pow_succ]

Premises used: Ideal.IsTwoSided.pow_succ
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
⊢ Jac ^ (n + 1) = Jac ^ n

Tactic:
(hn _ n.le_succ).symm

Premises used: Nat.le_succ, OrderDual, Eq.symm
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
⊢ Jac ^ (n + 1) = Jac ^ n

Tactic:
exact (hn _ n.le_succ).symm

Premises used: Nat.le_succ, Eq.symm
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
⊢ Jac * Jac ^ n = Jac ^ n

Tactic:
have hn : Jac * Jac ^ n = Jac ^ n := by
      rw [← Ideal.IsTwoSided.pow_succ]; exact (hn _ n.le_succ).symm
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
h : HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
⊢ IsNilpotent (R := Ideal R) (Ring.jacobson R)

Tactic:
use n
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
h : ∀ (ne : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0), False
⊢ HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0

Tactic:
by_contra ne
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
h :
  ∀ (N : Ideal R) (eq : Jac * N = N) (ne : N ≠ ⊥)
    (min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N), False
⊢ False

Tactic:
have ⟨N, ⟨eq, ne⟩, min⟩ := wellFounded_lt.has_min {N | Jac * N = N ∧ N ≠ ⊥} ⟨_, hn, ne⟩
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
rw : 1 * N = N
rw₁ rw₂ : N = N
⊢ Jac ^ Nat.zero * N = N

Tactic:
rw [Jac.pow_zero, N.one_mul]

Premises used: Submodule.pow_zero, Submodule.one_mul