-- Mathlib/RingTheory/RingHom/Finite.lean
theorem RingHom.finite_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.Finite

Proof state:
case intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
this✝ :
  ∀ (r : { x // x ∈ s }),
    IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : ⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • (algebraMap S (Localization.Away (f ↑r))) x ∈ Submodule.span R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
dsimp only at hn₁

Result:
case intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
this✝ :
  ∀ (r : { x // x ∈ s }),
    IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : ⟨↑r ^ n₁, ⋯⟩ • (algebraMap S (Localization.Away (f ↑r))) x ∈ Submodule.span R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Proof state:
case fg_top
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
this✝ :
  ∀ (r : { x // x ∈ s }),
    IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
H : ∀ (r : { x // x ∈ s }), ⊤.FG
⊢ ⊤.FG

Tactic:
choose s₁ s₂ using H

Result:
case fg_top
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
this✝ :
  ∀ (r : { x // x ∈ s }),
    IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
⊢ ⊤.FG

Proof state:
case h
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
this✝ :
  ∀ (r : { x // x ∈ s }),
    IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑r ^ (n₂ + n₁) • x ∈
    Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S) ↑r)) (s₁ r))
⊢ ↑r ^ (n₂ + n₁) • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
exact le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂

Result:
no goals