awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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))
    ⊤

Tactic:
Submodule.eq_top_of_localization_maximal Rₚ Mₚ f _ fun P hP ↦ ?_

Premises used: Submodule.eq_top_of_localization_maximal
-- 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 :
  ∀ (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)))
      ⊤
⊢ 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))
    ⊤

Tactic:
refine Submodule.eq_top_of_localization_maximal Rₚ Mₚ f _ fun P hP ↦ ?_

Premises used: Submodule.eq_top_of_localization_maximal
-- 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
P : Ideal R
hP : P.IsMaximal
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))
⊢ 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)))
    ⊤

Tactic:
rw [eq_top_iff, ← hs ⟨P, hP⟩, Submodule.localized'_span, Submodule.span_le]

Premises used: eq_top_iff, MaximalSpectrum.mk, Submodule.localized'_span, Submodule.span_le
-- 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
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))
⊢ Membership.mem (γ := Finset (Mₚ { asIdeal := P, isMaximal := hP }.asIdeal)) (s { asIdeal := P, isMaximal := hP }) x

Tactic:
hx
-- 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
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))
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))
⊢ 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))

Tactic:
lift x to s ⟨P, hP⟩ using hx

Premises used: MaximalSpectrum.mk
-- 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
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
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)
⊢ (↑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:
rw [SetLike.mem_coe, ← IsLocalization.smul_mem_iff (s := (frac ⟨P, hP⟩ x).2), hfrac]

Premises used: IsLocalization.smul_mem_iff, SetLike.mem_coe
-- 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
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ (frac { asIdeal := P, isMaximal := hP : MaximalSpectrum R } (↑x : Mₚ { asIdeal := P, isMaximal := hP }.asIdeal)).1 ∈
    (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
          Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
      Set M)

Tactic:
simpa using ⟨_, _, x.2, rfl⟩
-- 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
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ 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:
exact Submodule.subset_span ⟨_, by simpa using ⟨_, _, x.2, rfl⟩, rfl⟩
-- 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)
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)
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
⊢ N.FG

Tactic:
simp_rw [← Module.Finite.iff_fg] at ⊢ H

Premises used: Module.Finite.iff_fg
-- 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)
N : Submodule R M
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:
.of_isLocalized_maximal _ _ _ (fun P ↦ N.toLocalized' (Rₚ P) P.primeCompl (f P)) H

Premises used: Submodule.toLocalized', Module.Finite.of_isLocalized_maximal, Ideal.primeCompl
-- 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)
N : Submodule R M
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:
exact .of_isLocalized_maximal _ _ _ (fun P ↦ N.toLocalized' (Rₚ P) P.primeCompl (f P)) H
-- 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
H :
  ∀ (P : Ideal R) [inst_4 : P.IsMaximal],
    Module.Finite (Localization (M := R) P.primeCompl) (LocalizedModule P.primeCompl M)
⊢ Module.Finite R M

Tactic:
.of_isLocalized_maximal M _ _ (fun _ _ ↦ LocalizedModule.mkLinearMap _ _) H

Premises used: Module.Finite.of_isLocalized_maximal, LocalizedModule.mkLinearMap
-- 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
N : Submodule R M
H : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], (localized P.primeCompl N).FG
⊢ N.FG

Tactic:
N.fg_of_isLocalized_maximal _ _ _ H

Premises used: Submodule.fg_of_isLocalized_maximal