-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
obtain :
  ∀ (n₂ : ℕ)
    (hn₂ :
      Membership.mem (γ := Submodule R S)
        (Submodule.span R
          (↑(IsLocalization.finsetIntegerMultiple
                (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
            Set S))
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯ •
          HMul.hMul (α := S)
            ((algebraMap R S : (a : R) → S)
                (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                      ((↑r : R) ^ n₁) ⋯) :
                  R) :
              S)
            x)),
    ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)

Tactic:
obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R))
      (Localization.Away (f r)) _ (s₁ r) hn₁

Premises used: IsLocalization.smul_mem_finsetIntegerMultiple_span, Localization.Away, Submonoid.powers, Subtype.val, DFunLike.coe, rfl