awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
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
P : Ideal R
hP : P.IsMaximal
⊢ Eq (α := Submodule.{u_3, u_4} (Rₚ P) (Mₚ P))
    (Submodule.localized' (Rₚ P) P.primeCompl (f P)
      (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)))
    ⊤
have h : (↑(s { asIdeal := P, isMaximal := hP : MaximalSpectrum R }) : Set (Mₚ { asIdeal := P, isMaximal := hP }.asIdeal)) ⊆
  (↑(Submodule.span (Rₚ P)
        ((⇑(f P) : (a : M) → Mₚ P) ''
          (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
                Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
            Set M))) :
    Set (Mₚ { asIdeal := P, isMaximal := hP }.asIdeal))
Tactic: rw [eq_top_iff, ← hs ⟨P, hP⟩, Submodule.localized'_span, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
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
P : Ideal R
hP : P.IsMaximal
x : Mₚ { asIdeal := P, isMaximal := hP }.asIdeal
hx :
  x ∈ (↑(s { asIdeal := P, isMaximal := hP : MaximalSpectrum R }) : Set (Mₚ { asIdeal := P, isMaximal := hP }.asIdeal))
⊢ x ∈
    (↑(Submodule.span (Rₚ P)
          ((⇑(f P) : (a : M) → Mₚ P) ''
            (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
                  Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
              Set M))) :
      Set (Mₚ { asIdeal := P, isMaximal := hP }.asIdeal))
have h : ∀ (x : ↥(s { asIdeal := P, isMaximal := hP })),
  (↑x : Mₚ { asIdeal := P, isMaximal := hP }.asIdeal) ∈
    (↑(Submodule.span (Rₚ P)
          ((⇑(f P) : (a : M) → Mₚ P) ''
            (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
                  Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
              Set M))) :
      Set (Mₚ { asIdeal := P, isMaximal := hP }.asIdeal))
Tactic: lift x to s ⟨P, hP⟩ using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
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
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ (↑x : Mₚ { asIdeal := P, isMaximal := hP }.asIdeal) ∈
    (↑(Submodule.span (Rₚ P)
          ((⇑(f P) : (a : M) → Mₚ P) ''
            (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
                  Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
              Set M))) :
      Set (Mₚ { asIdeal := P, isMaximal := hP }.asIdeal))
have h : Membership.mem.{u_4, u_4} (α := Mₚ { asIdeal := P, isMaximal := hP }.asIdeal) (γ :=
  Submodule.{u_3, u_4} (Rₚ P) (Mₚ { asIdeal := P, isMaximal := hP }.asIdeal))
  (Submodule.span (Rₚ P)
    ((⇑(f P) : (a : M) → Mₚ P) ''
      (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
            Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
        Set M)))
  ((f { asIdeal := P, isMaximal := hP }.asIdeal : (a : M) → Mₚ { asIdeal := P, isMaximal := hP }.asIdeal)
      (frac { asIdeal := P, isMaximal := hP : MaximalSpectrum R }
          (↑x : Mₚ { asIdeal := P, isMaximal := hP }.asIdeal)).1 :
    Mₚ { asIdeal := P, isMaximal := hP }.asIdeal)
Tactic: rw [SetLike.mem_coe, ← IsLocalization.smul_mem_iff (s := (frac ⟨P, hP⟩ x).2), hfrac]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
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)
⊢ Module.Finite R M
have have : ∀ (this : Fintype (MaximalSpectrum R)), Module.Finite R M
Tactic: classical
  have : Fintype (MaximalSpectrum R) := Fintype.ofFinite _
  choose s hs using fun P : MaximalSpectrum R ↦ (H P.1).fg_top
  choose frac hfrac using fun P : MaximalSpectrum R ↦ IsLocalizedModule.surj P.1.primeCompl (f P.1)
  use Finset.biUnion Finset.univ fun P ↦ Finset.image (frac P · |>.1) (s P)
  refine Submodule.eq_top_of_localization_maximal Rₚ Mₚ f _ fun P hP ↦ ?_
  rw [eq_top_iff, ← hs ⟨P, hP⟩, Submodule.localized'_span, Submodule.span_le]
  intro x hx
  lift x to s ⟨P, hP⟩ using hx
  rw [SetLike.mem_coe, ← IsLocalization.smul_mem_iff (s := (frac ⟨P, hP⟩ x).2), hfrac]
  exact Submodule.subset_span ⟨_, by simpa using ⟨_, _, x.2, rfl⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
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 have₁ have₂ : ∀ (this : Fintype (MaximalSpectrum R)), Module.Finite R M
⊢ Module.Finite R M
have have₃ : ∀ (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))) ⊤),
  Module.Finite R M
Tactic: classical
  have : Fintype (MaximalSpectrum R) := Fintype.ofFinite _
  choose s hs using fun P : MaximalSpectrum R ↦ (H P.1).fg_top
  choose frac hfrac using fun P : MaximalSpectrum R ↦ IsLocalizedModule.surj P.1.primeCompl (f P.1)
  use Finset.biUnion Finset.univ fun P ↦ Finset.image (frac P · |>.1) (s P)
  refine Submodule.eq_top_of_localization_maximal Rₚ Mₚ f _ fun P hP ↦ ?_
  rw [eq_top_iff, ← hs ⟨P, hP⟩, Submodule.localized'_span, Submodule.span_le]
  intro x hx
  lift x to s ⟨P, hP⟩ using hx
  rw [SetLike.mem_coe, ← IsLocalization.smul_mem_iff (s := (frac ⟨P, hP⟩ x).2), hfrac]
  exact Submodule.subset_span ⟨_, by simpa using ⟨_, _, x.2, rfl⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
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 have₁ have₂ : ∀ (this : Fintype (MaximalSpectrum R)), Module.Finite R M
have₃ :
  ∀ (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))) ⊤),
    Module.Finite R M
⊢ Module.Finite R M
have have₄ : ∀ (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),
  Module.Finite R M
Tactic: classical
  have : Fintype (MaximalSpectrum R) := Fintype.ofFinite _
  choose s hs using fun P : MaximalSpectrum R ↦ (H P.1).fg_top
  choose frac hfrac using fun P : MaximalSpectrum R ↦ IsLocalizedModule.surj P.1.primeCompl (f P.1)
  use Finset.biUnion Finset.univ fun P ↦ Finset.image (frac P · |>.1) (s P)
  refine Submodule.eq_top_of_localization_maximal Rₚ Mₚ f _ fun P hP ↦ ?_
  rw [eq_top_iff, ← hs ⟨P, hP⟩, Submodule.localized'_span, Submodule.span_le]
  intro x hx
  lift x to s ⟨P, hP⟩ using hx
  rw [SetLike.mem_coe, ← IsLocalization.smul_mem_iff (s := (frac ⟨P, hP⟩ x).2), hfrac]
  exact Submodule.subset_span ⟨_, by simpa using ⟨_, _, x.2, rfl⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
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)
N : Submodule R M
H :
  ∀ (P : Ideal R) [inst_12 : P.IsMaximal],
    FG.{u_3, u_4} (R := Rₚ P) (M := Mₚ P) (localized' (Rₚ P) P.primeCompl (f P) N)
⊢ N.FG
have simp_rw : ∀
  (H :
    ∀ (P : Ideal R) [inst_12 : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) ↥(localized' (Rₚ P) P.primeCompl (f P) N)),
  Module.Finite.{u_1, u_2} R ↥N
Tactic: simp_rw [← Module.Finite.iff_fg] at ⊢ H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
⊢ IsPrincipalIdealRing R
have this : IsNoetherianRing R
Tactic: have : IsNoetherianRing R :=
    IsNoetherianRing.of_isLocalization_maximal Rₚ fun P _ => inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this : IsNoetherianRing R
⊢ IsIntegrallyClosed R
have refine : ∀ (P : Ideal R) (hP : P.IsMaximal), IsIntegrallyClosed.{u_2} (Rₚ P)
Tactic: refine IsIntegrallyClosed.of_isLocalization_maximal Rₚ fun P hP => ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this : IsNoetherianRing R
P : Ideal R
hP : P.IsMaximal
⊢ IsIntegrallyClosed.{u_2} (Rₚ P)
have this₁ : IsDomain.{u_2} (Rₚ P)
Tactic: have : IsDomain (Rₚ P) := IsLocalization.isDomain_of_atPrime (Rₚ P) P
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this : IsNoetherianRing R
⊢ IsPrincipalIdealRing R
have this₁ : IsIntegrallyClosed R
Tactic: have : IsIntegrallyClosed R := by
    refine IsIntegrallyClosed.of_isLocalization_maximal Rₚ fun P hP => ?_
    have : IsDomain (Rₚ P) := IsLocalization.isDomain_of_atPrime (Rₚ P) P
    infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this : IsIntegrallyClosed R
⊢ IsPrincipalIdealRing R
have this₁ : Ring.KrullDimLE 1 R
Tactic: have : Ring.KrullDimLE 1 R :=
    Ring.krullDimLE_of_isLocalization_maximal Rₚ fun P _ => inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : Ring.KrullDimLE 1 R
⊢ IsPrincipalIdealRing R
have this₁ : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
Tactic: rw [Ring.krullDimLE_one_iff_of_noZeroDivisors] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
⊢ IsPrincipalIdealRing R
have dedekind : IsDedekindDomain R
Tactic: have dedekind : IsDedekindDomain R := { maximalOfPrime := this _ }
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
⊢ Set.Finite.{u_1} (α := Ideal R) {P : Ideal R | P.IsMaximal}
have rw : Set.Finite.{u_1} (α := Ideal R) (Set.range MaximalSpectrum.asIdeal)
Tactic: rw [← MaximalSpectrum.range_asIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_3 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Algebra.{u_1, u_2} R (Rₚ P)
inst_4 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_2} (Rₚ P) P
inst_5 : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing.{u_2} (Rₚ P)
this_1 : IsNoetherianRing R
this_2 : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
⊢ IsPrincipalIdealRing R
have hp_finite : Set.Finite.{u_1} (α := Ideal R) {P : Ideal R | P.IsMaximal}
Tactic: have hp_finite : {P : Ideal R | P.IsMaximal}.Finite := by
    rw [← MaximalSpectrum.range_asIdeal]
    exact Set.finite_range MaximalSpectrum.asIdeal