awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Module
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ StableUnderSpecialization (X := PrimeSpectrum R) (support R M)

Tactic:
fun x y e ↦ mem_support_mono <| (PrimeSpectrum.le_iff_specializes x y).mpr e

Premises used: Iff.mpr, StableUnderSpecialization, Module.mem_support_mono, PrimeSpectrum.le_iff_specializes
-- Module: Mathlib.RingTheory.Spectrum.Prime.Module
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
rw : IsClosed (X := PrimeSpectrum R) (PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R))
⊢ IsClosed (X := PrimeSpectrum R) (support R M)

Tactic:
rw [support_eq_zeroLocus]

Premises used: Module.support_eq_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.Module
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
⊢ IsClosed (X := PrimeSpectrum R) (PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R))

Tactic:
apply PrimeSpectrum.isClosed_zeroLocus

Premises used: PrimeSpectrum.isClosed_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.Module
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (support A M) x
simp :
  ∀ (hx : ∃ (m : M), ∀ (r : A), r • m = 0 → r ∈ x.asIdeal),
    ∃ (m : M), ∀ (r : R), r • m = 0 → Membership.mem (α := A) x.asIdeal ((algebraMap R A : (a : R) → A) r : A)
⊢ Membership.mem (γ := Set (PrimeSpectrum A))
    (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R A)) (support R M)) x

Tactic:
simp only [Set.mem_preimage, mem_support_iff', PrimeSpectrum.comap_asIdeal, Ideal.mem_comap,
    ne_eq, not_imp_not] at hx ⊢

Premises used: Module.mem_support_iff', ne_eq, PrimeSpectrum.comap_asIdeal, Ideal.mem_comap, Set.mem_preimage, not_imp_not
-- Module: Mathlib.RingTheory.Spectrum.Prime.Module
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
x : PrimeSpectrum A
hx : ∃ (m : M), ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
obtain :
  ∀ (m : M) (hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal),
    ∃ (m : M), ∀ (r : R), r • m = 0 → Membership.mem (α := A) x.asIdeal ((algebraMap R A : (a : R) → A) r : A)
⊢ ∃ (m : M), ∀ (r : R), r • m = 0 → Membership.mem (α := A) x.asIdeal ((algebraMap R A : (a : R) → A) r : A)

Tactic:
obtain ⟨m, hm⟩ := hx
-- Module: Mathlib.RingTheory.Spectrum.Prime.Module
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
x : PrimeSpectrum A
m : M
hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
r : R
e : r • m = 0
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m = 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Spectrum.Prime.Module
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
x : PrimeSpectrum A
m : M
hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
⊢ ∃ (m : M), ∀ (r : R), r • m = 0 → Membership.mem (α := A) x.asIdeal ((algebraMap R A : (a : R) → A) r : A)

Tactic:
exact ⟨m, fun r e ↦ hm _ (by simpa)⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
⊢ NoetherianSpace.{u} (PrimeSpectrum R)

Tactic:
((noetherianSpace_TFAE <| PrimeSpectrum R).out 0 1).mpr (closedsEmbedding R).dual.wellFoundedLT

Premises used: Iff.mpr, TopologicalSpace.noetherianSpace_TFAE, List.TFAE.out, OrderEmbedding.wellFoundedLT, PrimeSpectrum, OfNat.ofNat, OrderEmbedding.dual, PrimeSpectrum.closedsEmbedding
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
⊢ Function.Injective.{u + 1, u + 1} (α := PrimeSpectrum R) asIdeal

Tactic:
have : Function.Injective (asIdeal (R := R)) := @PrimeSpectrum.ext _ _
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
this : Function.Injective.{u + 1, u + 1} (α := PrimeSpectrum R) asIdeal
⊢ Set.Finite.{u} (α := PrimeSpectrum R) {x : PrimeSpectrum R | IsMin x}

Tactic:
Set.Finite.of_finite_image (f := asIdeal) ?_ this.injOn

Premises used: Function.Injective.injOn, Set.Finite.of_finite_image
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
this : Function.Injective.{u + 1, u + 1} (α := PrimeSpectrum R) asIdeal
refine : Set.Finite.{u} (α := Ideal R) (asIdeal '' {x : PrimeSpectrum R | IsMin x})
⊢ Set.Finite.{u} (α := PrimeSpectrum R) {x : PrimeSpectrum R | IsMin x}

Tactic:
refine Set.Finite.of_finite_image (f := asIdeal) ?_ this.injOn

Premises used: Function.Injective.injOn, Set.Finite.of_finite_image
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
this : Function.Injective.{u + 1, u + 1} (α := PrimeSpectrum R) asIdeal
simp_rw :
  Set.Finite.{u} (α := Ideal R)
    (asIdeal '' {x : PrimeSpectrum R | Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x.asIdeal})
⊢ Set.Finite.{u} (α := Ideal R) (asIdeal '' {x : PrimeSpectrum R | IsMin x})

Tactic:
simp_rw [isMin_iff]

Premises used: PrimeSpectrum.isMin_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
this : Function.Injective.{u + 1, u + 1} (α := PrimeSpectrum R) asIdeal
⊢ Set.Finite.{u} (α := Ideal R)
    (asIdeal '' {x : PrimeSpectrum R | Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x.asIdeal})

Tactic:
(minimalPrimes.finite_of_isNoetherianRing R).subset (Set.image_preimage_subset _ _)

Premises used: minimalPrimes.finite_of_isNoetherianRing, Set.Finite.subset, Set.image_preimage_subset
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
this : Function.Injective.{u + 1, u + 1} (α := PrimeSpectrum R) asIdeal
⊢ Set.Finite.{u} (α := Ideal R)
    (asIdeal '' {x : PrimeSpectrum R | Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x.asIdeal})

Tactic:
exact (minimalPrimes.finite_of_isNoetherianRing R).subset (Set.image_preimage_subset _ _)

Premises used: minimalPrimes.finite_of_isNoetherianRing, Set.Finite.subset, Set.image_preimage_subset
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ Ring.KrullDimLE 0 R

Tactic:
.mk₀ fun _ _ ↦ inferInstance

Premises used: Ring.KrullDimLE.mk₀, inferInstance
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ DiscreteTopology.{u_1} (PrimeSpectrum R)

Tactic:
discreteTopology_iff_finite_and_krullDimLE_zero.mpr ⟨inferInstance, inferInstance⟩

Premises used: Iff.mpr, PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero, inferInstance, And.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
obtain :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)),
    ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Tactic:
obtain ⟨r, hr⟩ := PrimeSpectrum.toPiLocalization_bijective.2 (Pi.single ⟨p, inferInstance⟩ 1)

Premises used: PrimeSpectrum.mk, inferInstance, PrimeSpectrum.toPiLocalization_bijective, Pi.single, And.right, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
⊢ Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)

Tactic:
simpa [PrimeSpectrum.toPiLocalization,
      -FaithfulSMul.algebraMap_eq_one_iff] using funext_iff.mp hr ⟨p, inferInstance⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.toPiLocalization, funext_iff, inferInstance, FaithfulSMul.algebraMap_eq_one_iff, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
⊢ Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)

Tactic:
have : algebraMap R (Localization p.primeCompl) r = 1 := by
    simpa [PrimeSpectrum.toPiLocalization,
      -FaithfulSMul.algebraMap_eq_one_iff] using funext_iff.mp hr ⟨p, inferInstance⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Tactic:
⟨r, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
refine_1 : r ∉ p
refine_2 : IsIdempotentElem r
refine_3 : ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Tactic:
refine ⟨r, ?_, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
refine_1 : 1 ∉ IsLocalRing.maximalIdeal (Localization.AtPrime p)
⊢ r ∉ p

Tactic:
rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime p) p, this]

Premises used: Localization.AtPrime, IsLocalization.AtPrime.to_map_mem_maximal_iff, IsLocalization.AtPrime.isLocalRing
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
⊢ 1 ∉ IsLocalRing.maximalIdeal (Localization.AtPrime p)

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
refine_2 :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) (r * r) : PiLocalization R)
    ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
⊢ IsIdempotentElem r

Tactic:
apply PrimeSpectrum.toPiLocalization_bijective.injective

Premises used: PrimeSpectrum.toPiLocalization_bijective, Function.Bijective.injective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
⊢ Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) (r * r) : PiLocalization R)
    ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)

Tactic:
simp [map_mul, hr, ← Pi.single_mul]

Premises used: map_mul, Pi.single_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
q : Ideal R
hq : q.IsPrime
e : q ≠ p
⊢ { asIdeal := q, isPrime := ⋯ : PrimeSpectrum R } ≠ { asIdeal := p, isPrime := ⋯ }

Tactic:
have : PrimeSpectrum.mk q inferInstance ≠ ⟨p, inferInstance⟩ := ne_of_apply_ne (·.1) e
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this_1 :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this : { asIdeal := q, isPrime := ⋯ : PrimeSpectrum R } ≠ { asIdeal := p, isPrime := ⋯ }
⊢ Eq (α := Localization.AtPrime q)
    ((algebraMap R (Localization.AtPrime q) : (a : R) → Localization.AtPrime q) r : Localization.AtPrime q)
    (0 : Localization.AtPrime q)

Tactic:
simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.toPiLocalization, funext_iff, inferInstance, Iff.mp, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this_1 :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this : { asIdeal := q, isPrime := ⋯ : PrimeSpectrum R } ≠ { asIdeal := p, isPrime := ⋯ }
⊢ Eq (α := Localization.AtPrime q)
    ((algebraMap R (Localization.AtPrime q) : (a : R) → Localization.AtPrime q) r : Localization.AtPrime q)
    (0 : Localization.AtPrime q)

Tactic:
have : (algebraMap R (Localization.AtPrime q)) r = 0 := by
      simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this_1 :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this_2 : { asIdeal := q, isPrime := ⋯ : PrimeSpectrum R } ≠ { asIdeal := p, isPrime := ⋯ }
this :
  Eq (α := Localization.AtPrime q)
    ((algebraMap R (Localization.AtPrime q) : (a : R) → Localization.AtPrime q) r : Localization.AtPrime q)
    (0 : Localization.AtPrime q)
refine_3 : Membership.mem (γ := Ideal (Localization.AtPrime q)) (IsLocalRing.maximalIdeal (Localization.AtPrime q)) 0
⊢ r ∈ q

Tactic:
rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime q) q, this]

Premises used: Localization.AtPrime, IsLocalization.AtPrime.to_map_mem_maximal_iff, IsLocalization.AtPrime.isLocalRing
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this_1 :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this_2 : { asIdeal := q, isPrime := ⋯ : PrimeSpectrum R } ≠ { asIdeal := p, isPrime := ⋯ }
this :
  Eq (α := Localization.AtPrime q)
    ((algebraMap R (Localization.AtPrime q) : (a : R) → Localization.AtPrime q) r : Localization.AtPrime q)
    (0 : Localization.AtPrime q)
⊢ Membership.mem (γ := Ideal (Localization.AtPrime q)) (IsLocalRing.maximalIdeal (Localization.AtPrime q)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
F : Type u_2
inst_2 : Field F
inst_3 : Algebra F R
inst_4 : Module.Finite F R
inst_5 : Fintype (PrimeSpectrum R)
⊢ Module.finrank F R = ∑ p : PrimeSpectrum R, Module.finrank.{u_2, u_1} F (Localization.AtPrime p.asIdeal)

Tactic:
have (p : Ideal R) [p.IsPrime] : Module.Finite F (Localization.AtPrime p) :=
    Module.Finite.of_surjective (Algebra.algHom F R (Localization.AtPrime p)).toLinearMap
      (localization_surjective p.primeCompl (Localization.AtPrime p))
  ((toPiLocalizationEquiv R).restrictScalars F).toLinearEquiv.finrank_eq.trans
    (Module.finrank_pi_fintype F)

Premises used: AlgHom.toLinearMap, Module.Finite.of_surjective, IsArtinianRing.localization_surjective, Localization.AtPrime, LinearEquiv.finrank_eq, AlgEquiv.restrictScalars, Module.finrank_pi_fintype, Algebra.algHom, AlgEquiv.toLinearEquiv, Ideal.primeCompl, PrimeSpectrum.toPiLocalizationEquiv, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
inl :
  Subsingleton R →
    (IsNilpotent (R := A ⊗[R] I.ResidueField)
        ((algebraMap A (A ⊗[R] I.ResidueField) : (a : A) → A ⊗[R] I.ResidueField) f : A ⊗[R] I.ResidueField) ↔
      ∀ i < Module.finrank R A,
        coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) i ∈ I)
inr :
  Nontrivial R →
    (IsNilpotent (R := A ⊗[R] I.ResidueField)
        ((algebraMap A (A ⊗[R] I.ResidueField) : (a : A) → A ⊗[R] I.ResidueField) f : A ⊗[R] I.ResidueField) ↔
      ∀ i < Module.finrank R A,
        coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) i ∈ I)
⊢ IsNilpotent (R := A ⊗[R] I.ResidueField)
      ((algebraMap A (A ⊗[R] I.ResidueField) : (a : A) → A ⊗[R] I.ResidueField) f : A ⊗[R] I.ResidueField) ↔
    ∀ i < Module.finrank R A,
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) i ∈ I

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Subsingleton R
⊢ Subsingleton (A ⊗[R] I.ResidueField)

Tactic:
have := (algebraMap R (A ⊗[R] I.ResidueField)).codomain_trivial