-- Mathlib/RingTheory/RingHom/Finite.lean
lemma Module.Finite_of_isLocalization (R S Rₚ Sₚ) [CommSemiring R] [CommRing S] [CommRing Rₚ]
    [CommRing Sₚ] [Algebra R S] [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ]
    [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] (M : Submonoid R) [IsLocalization M Rₚ]
    [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [hRS : Module.Finite R S] :
    Module.Finite Rₚ Sₚ

Proof state:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ Module.Finite Rₚ Sₚ

Tactic:
obtain ⟨T, hT⟩ := hRS

Result:
case mk.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
T : Finset S
hT : Submodule.span R ↑T = ⊤
⊢ Module.Finite Rₚ Sₚ

Proof state:
case h.intro.intro.mk.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
T : Finset S
hT : Submodule.span R ↑T = ⊤
y : S
r : R
hr : r ∈ ↑M
hy : (algebraMap S Sₚ) y ∈ Submodule.span R (⇑(IsScalarTower.toAlgHom R S Sₚ).toLinearMap '' ↑T)
H :
  Submodule.span R (⇑(algebraMap S Sₚ) '' ↑T) ≤
    Submodule.restrictScalars R (Submodule.span Rₚ (⇑(algebraMap S Sₚ) '' ↑T))
⊢ IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) r, ⋯⟩ * (algebraMap S Sₚ) y ∈ Submodule.span Rₚ (⇑(algebraMap S Sₚ) '' ↑T)

Tactic:
convert (Submodule.span Rₚ (algebraMap S Sₚ '' T)).smul_mem
  (IsLocalization.mk' Rₚ (1 : R) ⟨r, hr⟩) (H hy) using 1

Result:
case h.e'_5
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
T : Finset S
hT : Submodule.span R ↑T = ⊤
y : S
r : R
hr : r ∈ ↑M
hy : (algebraMap S Sₚ) y ∈ Submodule.span R (⇑(IsScalarTower.toAlgHom R S Sₚ).toLinearMap '' ↑T)
H :
  Submodule.span R (⇑(algebraMap S Sₚ) '' ↑T) ≤
    Submodule.restrictScalars R (Submodule.span Rₚ (⇑(algebraMap S Sₚ) '' ↑T))
⊢ IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) r, ⋯⟩ * (algebraMap S Sₚ) y =
    IsLocalization.mk' Rₚ 1 ⟨r, hr⟩ • (algebraMap S Sₚ) y

Proof state:
case mk.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
T : Finset S
hT : Submodule.span R ↑T = ⊤
⊢ Module.Finite Rₚ Sₚ

Tactic:
use T.image (algebraMap S Sₚ)

Result:
case h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
T : Finset S
hT : Submodule.span R ↑T = ⊤
⊢ Submodule.span Rₚ ↑(Finset.image (⇑(algebraMap S Sₚ)) T) = ⊤

Proof state:
case h.intro.intro.mk.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
T : Finset S
hT : Submodule.span R ↑T = ⊤
y : S
r : R
hr : r ∈ ↑M
hy : (algebraMap S Sₚ) y ∈ Submodule.map (IsScalarTower.toAlgHom R S Sₚ).toLinearMap (Submodule.span R ↑T)
⊢ IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) r, ⋯⟩ * (algebraMap S Sₚ) y ∈ Submodule.span Rₚ (⇑(algebraMap S Sₚ) '' ↑T)

Tactic:
rw [Submodule.map_span (IsScalarTower.toAlgHom R S Sₚ).toLinearMap T] at hy

Result:
case h.intro.intro.mk.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
T : Finset S
hT : Submodule.span R ↑T = ⊤
y : S
r : R
hr : r ∈ ↑M
hy : (algebraMap S Sₚ) y ∈ Submodule.span R (⇑(IsScalarTower.toAlgHom R S Sₚ).toLinearMap '' ↑T)
⊢ IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) r, ⋯⟩ * (algebraMap S Sₚ) y ∈ Submodule.span Rₚ (⇑(algebraMap S Sₚ) '' ↑T)

Proof state:
case h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
T : Finset S
hT : Submodule.span R ↑T = ⊤
⊢ Submodule.span Rₚ ↑(Finset.image (⇑(algebraMap S Sₚ)) T) = ⊤

Tactic:
rw [eq_top_iff]

Result:
case h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
T : Finset S
hT : Submodule.span R ↑T = ⊤
⊢ ⊤ ≤ Submodule.span Rₚ ↑(Finset.image (⇑(algebraMap S Sₚ)) T)