-- 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 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
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
h :
  ∀ (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))
      ⊤
h₁ :
  ∀ (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)))
      ⊤
h₂ :
  ∀ (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),
    (↑(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))
h₃ :
  ∀ (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))
h₄ :
  ∀ (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))
h₅ :
  ∀ (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)
⊢ 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⟩

Premises used: MaximalSpectrum.asIdeal, Module.Finite.fg_top, eq_top_iff, Submodule.localized'_span, SetLike.mem_coe, Ideal.primeCompl, Submodule.eq_top_of_localization_maximal, Submodule.span_le, IsLocalizedModule.surj