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

Tactic:
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

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

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ₚ
hRS : Module.Finite R S
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)

Tactic:
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

Result:
no goals

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:
rintro x -

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 = ⊤
x : Sₚ
⊢ x ∈ Submodule.span Rₚ ↑(Finset.image (⇑(algebraMap S Sₚ)) T)

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

Tactic:
exact Submodule.subset_span

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ₚ
hRS : Module.Finite R S
⊢ algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯

Tactic:
apply IsLocalization.ringHom_ext M

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ₚ
hRS : Module.Finite R S
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)

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
⊢ y ∈ ⊤

Tactic:
trivial

Result:
no goals