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

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₂ :
  ↑r ^ (n₂ + n₁) • x ∈
    Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S) ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))

Tactic:
use n₂ + n₁

Result:
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 }), 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.powers ((algebraMap R S) ↑r)) (s₁ r))
⊢ ↑r ^ (n₂ + 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 = ⊤
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 ∈ ⊤

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 = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
⊢ f.FiniteType

Tactic:
letI := f.toAlgebra

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
⊢ f.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:
rw [eq_top_iff]

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, Algebra.adjoin R ↑(sf x)

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

Tactic:
convert (Algebra.adjoin_attach_biUnion (R := R) sf).trans _

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, Algebra.adjoin R ↑(sf x) = ⊤