awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
p : Ideal R
hp : p.IsMaximal
⊢ Subsingleton (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
h ⟨p, hp⟩

Premises used: MaximalSpectrum.mk
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
p : Ideal R
hp : p.IsMaximal
⊢ Subsingleton (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
exact h ⟨p, hp⟩

Premises used: MaximalSpectrum.mk
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑⊤ : WithBot ℕ∞)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
n : ℕ
⊢ projectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑(↑n : ℕ∞) : WithBot ℕ∞)

Tactic:
simpa using aux n
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : ℕ∞
coe :
  projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑⊤ : WithBot ℕ∞)
coe₁ :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑(↑n : ℕ∞) : WithBot ℕ∞)
⊢ projectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)

Tactic:
induction N with
    | top => simp
    | coe n => simpa using aux n
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
bot :
  projectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
coe :
  ∀ (N : ℕ∞),
    projectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
      ⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl) ≤
        (↑N : WithBot ℕ∞)
⊢ projectiveDimension M ≤ N ↔
    ⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N

Tactic:
induction N with
  | bot =>
    simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, Module.subsingleton_of_localization_maximal, LocalizedModule, Equiv.subsingleton_congr, CategoryTheory.projectiveDimension_eq_bot_iff, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl, ModuleCat.localizedModule, equivShrink, iSup_eq_bot
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
eq_zero : ∀ (x : S), IsNilpotent x → x = 0
⊢ IsReduced S

Tactic:
constructor
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
e : HPow.hPow (β := ℕ) x 0 = 0
⊢ x = 0

Tactic:
simpa using congr_arg (· * x) e

Premises used: HMul.hMul, congr_arg
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
eq_zero :
  ∀ (y : R) (m : ↥M)
    (hx :
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, m).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (y, m).1),
    x = 0
⊢ x = 0

Tactic:
obtain ⟨⟨y, m⟩, hx⟩ := IsLocalization.surj M x

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq.{u_1 + 1} (α := S)
  ((fun (x : S) ↦ x ^ n.succ) (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S)))
  ((fun (x : S) ↦ x ^ n.succ) ((algebraMap R S : (a : R) → S) y)) :=
  ⋯
⊢ Eq (α := S) (0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)

Tactic:
simp only [mul_pow, e, zero_mul, ← map_pow] at hx'

Premises used: MulZeroClass.zero_mul, map_pow, mul_pow
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) (0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
⊢ Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)

Tactic:
rw [← (algebraMap R S).map_zero] at hx'

Premises used: Algebra.algebraMap, RingHom.map_zero
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
eq_zero : ∀ (m' : ↥M) (hm' : (↑m' : R) * 0 = (↑m' : R) * y ^ n.succ), x = 0
⊢ x = 0

Tactic:
obtain ⟨m', hm'⟩ := (IsLocalization.eq_iff_exists M S).mp hx'

Premises used: Iff.mp, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : (↑m' : R) * 0 = (↑m' : R) * y ^ n.succ
⊢ (↑m' : R) * 0 * (↑m' : R) ^ n = (↑m' : R) * y ^ n.succ * (↑m' : R) ^ n

Tactic:
apply_fun (· * (m' : R) ^ n) at hm'

Premises used: HMul.hMul, HPow.hPow, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : (↑m' : R) * 0 * (↑m' : R) ^ n = (↑m' : R) * y ^ n.succ * (↑m' : R) ^ n
⊢ 0 = (↑m' : R) * (y ^ n.succ * (↑m' : R) ^ n)

Tactic:
simp only [mul_assoc, zero_mul, mul_zero] at hm'

Premises used: MulZeroClass.zero_mul, mul_assoc, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : 0 = (↑m' : R) * (y ^ n.succ * (↑m' : R) ^ n)
⊢ 0 = (y * (↑m' : R)) ^ n.succ

Tactic:
rw [← mul_left_comm, ← pow_succ', ← mul_pow] at hm'

Premises used: mul_left_comm, mul_pow, pow_succ'
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : 0 = (y * (↑m' : R)) ^ n.succ
⊢ y * (↑m' : R) = 0

Tactic:
replace hm' := IsNilpotent.eq_zero ⟨_, hm'.symm⟩
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : y * (↑m' : R) = 0
eq_zero : ∃ (m : ↥M), (↑m : R) * y = 0
⊢ x = 0

Tactic:
rw [← (IsLocalization.map_units S m).mul_left_inj, hx, zero_mul,
    IsLocalization.map_eq_zero_iff M]

Premises used: IsLocalization.map_eq_zero_iff, MulZeroClass.zero_mul, IsLocalization.map_units, IsUnit.mul_left_inj
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : y * (↑m' : R) = 0
rw : (↑m' : R) * y = y * (↑m' : R)
rw₁ rw₂ : y * (↑m' : R) = y * (↑m' : R)
⊢ (↑m' : R) * y = 0

Tactic:
rw [← hm', mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : y * (↑m' : R) = 0
⊢ ∃ (m : ↥M), (↑m : R) * y = 0

Tactic:
exact ⟨m', by rw [← hm', mul_comm]⟩
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsReduced R
⊢ IsReduced.{u_1} (Localization (M := R) M)

Tactic:
isReduced_localizationPreserves M _ inferInstance

Premises used: inferInstance, isReduced_localizationPreserves
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
inst : CommRing R
h :
  ∀ (J : Ideal R) (x : J.IsMaximal),
    (fun (R : Type u_1) (x : CommRing R) ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
eq_zero : ∀ (x : R), IsNilpotent x → x = 0
⊢ IsReduced R

Tactic:
constructor
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
inst : CommRing R
h :
  ∀ (J : Ideal R) (x : J.IsMaximal),
    (fun (R : Type u_1) (x : CommRing R) ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
eq_zero :
  ∀ (J : Ideal R) (x_1 : J.IsMaximal),
    Eq (α := Localization.AtPrime J)
      ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x : Localization.AtPrime J)
      (0 : Localization.AtPrime J)
⊢ x = 0

Tactic:
apply eq_zero_of_localization

Premises used: eq_zero_of_localization
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
inst : CommRing R
h :
  ∀ (J : Ideal R) (x : J.IsMaximal),
    (fun (R : Type u_1) (x : CommRing R) ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
⊢ IsReduced.{u_1} (Localization.AtPrime J)

Tactic:
specialize h J hJ
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
h : IsReduced.{u_1} (Localization.AtPrime J)
⊢ Eq (α := Localization.AtPrime J)
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x : Localization.AtPrime J)
    (0 : Localization.AtPrime J)

Tactic:
(hx.map <| algebraMap R <| Localization.AtPrime J).eq_zero

Premises used: Algebra.algebraMap, Localization.AtPrime, IsNilpotent.map, IsNilpotent.eq_zero
-- Module: Mathlib.RingTheory.LocalProperties.Reduced
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
h : IsReduced.{u_1} (Localization.AtPrime J)
⊢ Eq (α := Localization.AtPrime J)
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x : Localization.AtPrime J)
    (0 : Localization.AtPrime J)

Tactic:
exact (hx.map <| algebraMap R <| Localization.AtPrime J).eq_zero

Premises used: Algebra.algebraMap, Localization.AtPrime, IsNilpotent.map, IsNilpotent.eq_zero
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_5 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_3, u_4} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_12 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) M (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) (Mₚ P)
have : ∀ (this : Fintype (MaximalSpectrum R)), Module.Finite R M
⊢ Module.Finite R M

Tactic:
have : Fintype (MaximalSpectrum R) := Fintype.ofFinite _
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_5 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_3, u_4} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_12 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) M (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
choose :
  ∀ (s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal))
    (hs :
      ∀ (P : MaximalSpectrum R),
        Eq (α := Submodule.{u_3, u_4} (Rₚ P.asIdeal) (Mₚ P.asIdeal))
          (Submodule.span (Rₚ P.asIdeal) (↑(s P) : Set (Mₚ P.asIdeal))) ⊤),
    Module.Finite R M
⊢ Module.Finite R M

Tactic:
choose s hs using fun P : MaximalSpectrum R ↦ (H P.1).fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_5 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_3, u_4} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_12 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) M (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs :
  ∀ (P : MaximalSpectrum R),
    Eq (α := Submodule.{u_3, u_4} (Rₚ P.asIdeal) (Mₚ P.asIdeal))
      (Submodule.span (Rₚ P.asIdeal) (↑(s P) : Set (Mₚ P.asIdeal))) ⊤
choose :
  ∀ (frac : (P : MaximalSpectrum R) → (y : Mₚ P.asIdeal) → Prod.{u_2, u_1} M ↥P.asIdeal.primeCompl)
    (hfrac :
      ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal),
        (frac P y).2 • y = (f P.asIdeal : (a : M) → Mₚ P.asIdeal) (frac P y).1),
    Module.Finite R M
⊢ Module.Finite R M

Tactic:
choose frac hfrac using fun P : MaximalSpectrum R ↦ IsLocalizedModule.surj P.1.primeCompl (f P.1)

Premises used: MaximalSpectrum.asIdeal, Ideal.primeCompl, IsLocalizedModule.surj
-- Module: Mathlib.RingTheory.LocalProperties.Semilocal
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_5 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_3, u_4} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_12 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) M (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs :
  ∀ (P : MaximalSpectrum R),
    Eq (α := Submodule.{u_3, u_4} (Rₚ P.asIdeal) (Mₚ P.asIdeal))
      (Submodule.span (Rₚ P.asIdeal) (↑(s P) : Set (Mₚ P.asIdeal))) ⊤
frac : (P : MaximalSpectrum R) → (y : Mₚ P.asIdeal) → Prod.{u_2, u_1} M ↥P.asIdeal.primeCompl
hfrac :
  ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal : (a : M) → Mₚ P.asIdeal) (frac P y).1
h :
  Eq (α := Submodule R M)
    (Submodule.span R
      (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
            Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
        Set M))
    ⊤
⊢ Module.Finite R M

Tactic:
use Finset.biUnion Finset.univ fun P ↦ Finset.image (frac P · |>.1) (s P)

Premises used: Finset.univ, Finset.biUnion, Prod.fst, Finset.image