-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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
⊢ Module.Finite R M
have 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)
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₂