-- 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
⊢ Module.Finite Rₚ Sₚ

Tactic:
classical
have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
    (algebraMap R S) (Submonoid.le_comap_map M) := by
  apply IsLocalization.ringHom_ext M
  simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
obtain ⟨T, hT⟩ := hRS
use T.image (algebraMap S Sₚ)
rw [eq_top_iff]
rintro x -
obtain ⟨y, ⟨_, ⟨r, hr, rfl⟩⟩, rfl⟩ :=
  IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid S M) x
rw [IsLocalization.mk'_eq_mul_mk'_one, mul_comm, Finset.coe_image]
have hy : y ∈ Submodule.span R ↑T := by rw [hT]; trivial
replace hy : algebraMap S Sₚ y ∈ Submodule.map (IsScalarTower.toAlgHom R S Sₚ).toLinearMap
  (Submodule.span R (T : Set S)) := Submodule.mem_map_of_mem
(f := (IsScalarTower.toAlgHom R S Sₚ).toLinearMap) hy
rw [Submodule.map_span (IsScalarTower.toAlgHom R S Sₚ).toLinearMap T] at hy
have H : Submodule.span R (algebraMap S Sₚ '' T) ≤
    (Submodule.span Rₚ (algebraMap S Sₚ '' T)).restrictScalars R := by
  rw [Submodule.span_le]; exact Submodule.subset_span
convert (Submodule.span Rₚ (algebraMap S Sₚ '' T)).smul_mem
  (IsLocalization.mk' Rₚ (1 : R) ⟨r, hr⟩) (H hy) using 1
rw [Algebra.smul_def, this, IsLocalization.map_mk', map_one]

Result:
no goals

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ₚ
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)
⊢ Submodule.span R (⇑(algebraMap S Sₚ) '' ↑T) ≤
    Submodule.restrictScalars R (Submodule.span Rₚ (⇑(algebraMap S Sₚ) '' ↑T))

Tactic:
rw [Submodule.span_le]

Result:
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)
⊢ ⇑(algebraMap S Sₚ) '' ↑T ⊆ ↑(Submodule.restrictScalars R (Submodule.span Rₚ (⇑(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.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)

Tactic:
have H : Submodule.span R (algebraMap S Sₚ '' T) ≤
    (Submodule.span Rₚ (algebraMap S Sₚ '' T)).restrictScalars R := by
  rw [Submodule.span_le]; exact Submodule.subset_span

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

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
⊢ IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) r, ⋯⟩ * (algebraMap S Sₚ) y ∈ Submodule.span Rₚ (⇑(algebraMap S Sₚ) '' ↑T)

Tactic:
have hy : y ∈ Submodule.span R ↑T := by rw [hT]; trivial

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 : y ∈ Submodule.span R ↑T
⊢ IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) r, ⋯⟩ * (algebraMap S Sₚ) y ∈ Submodule.span Rₚ (⇑(algebraMap S Sₚ) '' ↑T)