-- Mathlib/RingTheory/RingHom/FiniteType.lean
theorem finiteType_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.FiniteType

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 }), Algebra.adjoin (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) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))

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

Result:
case intro.mk.intro.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 }), Algebra.adjoin (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) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ⟨(fun x => ↑r ^ x) n₂, ⋯⟩ • ((algebraMap R S) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈
    Algebra.adjoin R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
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
r : { x // x ∈ s }
⊢ IsLocalization (Submonoid.powers ((algebraMap R S) ↑r)) (Localization.Away (f ↑r))

Tactic:
exact Localization.isLocalization

Result:
no goals

Proof state:
case intro.mk.intro.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 }), Algebra.adjoin (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) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ⟨(fun x => ↑r ^ x) n₂, ⋯⟩ • ((algebraMap R S) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈
    Algebra.adjoin R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))

Tactic:
rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂

Result:
case intro.mk.intro.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 }), Algebra.adjoin (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) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑r ^ (n₂ + n₁) • x ∈
    Algebra.adjoin R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))

Proof state:
⊢ OfLocalizationSpan @FiniteType

Tactic:
rw [RingHom.ofLocalizationSpan_iff_finite]

Result:
⊢ OfLocalizationFiniteSpan @FiniteType

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
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
r : { x // x ∈ s }
⊢ IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))

Tactic:
rw [Submonoid.map_powers]

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
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
r : { x // x ∈ s }
⊢ IsLocalization (Submonoid.powers ((algebraMap R S) ↑r)) (Localization.Away (f ↑r))