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

Proof state:
case h.convert_2
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, Algebra.adjoin R ↑(sf x)

Tactic:
rintro x -

Result:
case h.convert_2
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
⊢ x ∈ ⨆ x, Algebra.adjoin R ↑(sf x)

Proof state:
case out
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
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))
⊢ ⊤.FG

Tactic:
replace H := fun r => (H r).1

Result:
case out
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

Proof state:
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
⊢ (algebraMap S (Localization.Away (f ↑r))) x ∈ Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r)

Tactic:
rw [s₂ r]

Result:
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
⊢ (algebraMap S (Localization.Away (f ↑r))) x ∈ ⊤

Proof state:
case h.convert_2
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
⊢ x ∈ ⨆ x, Algebra.adjoin R ↑(sf x)

Tactic:
apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem
  _ hs _ _

Result:
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, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))