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

Proof state:
⊢ OfLocalizationSpan @Finite

Tactic:
classical
rw [RingHom.ofLocalizationSpan_iff_finite]
introv R hs H
letI := f.toAlgebra
letI := fun r : s => (Localization.awayMap f r).toAlgebra
have : ∀ r : s,
    IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S)) (Localization.Away (f r)) :=
  by intro r; rw [Submonoid.map_powers]; exact Localization.isLocalization
haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) :=
  fun r => IsScalarTower.of_algebraMap_eq'
    (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm
constructor
replace H := fun r => (H r).1
choose s₁ s₂ using H
let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)
use s.attach.biUnion sf
rw [Submodule.span_attach_biUnion, eq_top_iff]
rintro x -
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _
intro r
obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
  multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R))
    (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x)
    (by rw [s₂ r]; trivial)
dsimp only at hn₁
rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
  IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R))
    (Localization.Away (f r)) _ (s₁ r) hn₁
rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
simp_rw [Submonoid.map_powers] at hn₂
use n₂ + n₁
exact le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂

Result:
no goals

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).Finite
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 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

Tactic:
let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)

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) = ⊤
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
⊢ ⊤.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 }), 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
⊢ (algebraMap S (Localization.Away (f ↑r))) x ∈ ⊤

Tactic:
trivial

Result:
no goals

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 }), 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, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
  multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R))
    (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x)
    (by rw [s₂ r]; trivial)

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₁ : ⟨(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)

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).Finite
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).Finite
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))