-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
fg_top : Submodule.FG.{u, w} (R := R) (M := M) ⊤
fg_top₁ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    Submodule.FG.{u, w} (R := R) (M := M) ⊤
fg_top₂ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    Submodule.FG.{u, w} (R := R) (M := M) ⊤
h :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    Eq (α := Submodule R M) (Submodule.span R (↑(t.attach.biUnion sf) : Set M)) ⊤
h₁ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    LE.le.{w} (α := Submodule R M) ⊤ (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M))
h₂ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    ∀ ⦃x : M⦄, Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) x
h₃ h₄ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    ∀ ⦃x : M⦄ (r : (↑(↑t : Set R) : Type u)),
      ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
h₅ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    ∀ ⦃x : M⦄ (r : (↑(↑t : Set R) : Type u)),
      let S : Submonoid R := Submonoid.powers (↑r : R);
      ∀ (n₁ : ℕ)
        (hn₁ :
          Membership.mem (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
            (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯ •
              IsLocalizedModule.mk' (S := S) (f r) x 1)),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
h₆ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    ∀ ⦃x : M⦄ (r : (↑(↑t : Set R) : Type u)),
      let S : Submonoid R := Submonoid.powers (↑r : R);
      ∀ (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
            ((f r : (a : M) → Mₚ r)
                ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
              Mₚ r)),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
h₇ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    ∀ ⦃x : M⦄ (r : (↑(↑t : Set R) : Type u)),
      let S : Submonoid R := Submonoid.powers (↑r : R);
      ∀ (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
            ((f r : (a : M) → Mₚ r)
                ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
              Mₚ r))
        (n₂ : ℕ)
        (hn₂ :
          Membership.mem (γ := Submodule R M)
            (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
            (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯ •
              (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
h₈ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    ∀ ⦃x : M⦄ (r : (↑(↑t : Set R) : Type u)),
      let S : Submonoid R := Submonoid.powers (↑r : R);
      ∀ (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
            ((f r : (a : M) → Mₚ r)
                ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
              Mₚ r))
        (n₂ : ℕ)
        (hn₂ :
          Membership.mem (γ := Submodule R M)
            (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
            ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
              (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
h₉ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    ∀ ⦃x : M⦄ (r : (↑(↑t : Set R) : Type u)),
      let S : Submonoid R := Submonoid.powers (↑r : R);
      ∀ (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
            ((f r : (a : M) → Mₚ r)
                ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
              Mₚ r))
        (n₂ : ℕ)
        (hn₂ :
          Membership.mem (γ := Submodule R M)
            (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
            ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
              (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)),
        Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ (n₂ + n₁) • x)
h₁₀ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    ∀ ⦃x : M⦄ (r : (↑(↑t : Set R) : Type u)),
      let S : Submonoid R := Submonoid.powers (↑r : R);
      ∀ (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
            ((f r : (a : M) → Mₚ r)
                ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
              Mₚ r))
        (n₂ : ℕ)
        (hn₂ :
          Membership.mem (γ := Submodule R M)
            (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
            ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
              (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)),
        Membership.mem (γ := Submodule R M) (Submodule.span R (↑(sf r) : Set M)) ((↑r : R) ^ (n₂ + n₁) • x)
h₁₁ :
  ∀ (s₁ : (g : ↥t) → Finset (Mₚ g))
    (s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤),
    let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
      IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
    ∀ ⦃x : M⦄ (r : (↑(↑t : Set R) : Type u)),
      let S : Submonoid R := Submonoid.powers (↑r : R);
      ∀ (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
            ((f r : (a : M) → Mₚ r)
                ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
              Mₚ r))
        (n₂ : ℕ)
        (hn₂ :
          Membership.mem (γ := Submodule R M)
            (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
            ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
              (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)),
        Membership.mem (γ := Submodule R M) (Submodule.span R (↑(sf r) : Set M)) ((↑r : R) ^ n₂ • (↑r : R) ^ n₁ • x)
⊢ Module.Finite R M

Tactic:
classical
  constructor
  choose s₁ s₂ using (fun g ↦ (H g).1)
  let sf := fun x : t ↦
    IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers x.val) (f x) (s₁ x)
  use t.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  rintro x -
  refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)
  set S : Submonoid R := Submonoid.powers r.val
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ := multiple_mem_span_of_mem_localization_span S (Rₚ r)
    (s₁ r : Set (Mₚ r)) (IsLocalizedModule.mk' (f r) x (1 : S)) (by rw [s₂ r]; trivial)
  rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalizedModule.smul_mem_finsetIntegerMultiple_span
    S (f r) _ (s₁ r) hn₁
  rw [Submonoid.smul_def] at hn₂
  use n₂ + n₁
  apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) r
  rw [pow_add, mul_smul]
  exact hn₂

Premises used: Submodule.mem_of_span_eq_top_of_smul_pow_mem, Module.Finite.fg_top, eq_top_iff, Submodule.span_attach_biUnion, pow_add, IsLocalizedModule.mk'_one, Submonoid.smul_def, SetLike.coe, IsLocalizedModule.mk'_smul, SemigroupAction.mul_smul, Submonoid, rfl