-- Mathlib/RingTheory/RingHom/Finite.lean
theorem RingHom.finite_localizationPreserves : RingHom.LocalizationPreserves @RingHom.Finite

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝² : Algebra R S := f.toAlgebra
this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝ : Algebra R' S' := f'.toAlgebra
this : IsScalarTower R R' S'
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
have : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' rfl

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝³ : Algebra R S := f.toAlgebra
this✝² : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝¹ : Algebra R' S' := f'.toAlgebra
this✝ : IsScalarTower R R' S'
this : IsScalarTower R S S'
⊢ (IsLocalization.map S' f ⋯).Finite

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝⁵ : Algebra R S := f.toAlgebra
this✝⁴ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝³ : Algebra R' S' := f'.toAlgebra
this✝² : IsScalarTower R R' S'
this✝¹ : IsScalarTower R S S'
this✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
this : Module.Finite R S
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
apply Module.Finite_of_isLocalization R S R' S' M

Result:
no goals

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝ : Algebra R S := f.toAlgebra
this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
let f' : R' →+* S' := IsLocalization.map S' f (Submonoid.le_comap_map M)

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝ : Algebra R S := f.toAlgebra
this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
⊢ (IsLocalization.map S' f ⋯).Finite

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝¹ : Algebra R S := f.toAlgebra
this✝ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this : Algebra R' S' := f'.toAlgebra
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
have : IsScalarTower R R' S' := IsScalarTower.of_algebraMap_eq'
  (IsLocalization.map_comp M.le_comap_map).symm

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝² : Algebra R S := f.toAlgebra
this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝ : Algebra R' S' := f'.toAlgebra
this : IsScalarTower R R' S'
⊢ (IsLocalization.map S' f ⋯).Finite

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝ : Algebra R S := f.toAlgebra
this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
letI := f'.toAlgebra

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝¹ : Algebra R S := f.toAlgebra
this✝ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this : Algebra R' S' := f'.toAlgebra
⊢ (IsLocalization.map S' f ⋯).Finite

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝³ : Algebra R S := f.toAlgebra
this✝² : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝¹ : Algebra R' S' := f'.toAlgebra
this✝ : IsScalarTower R R' S'
this : IsScalarTower R S S'
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) S'

Tactic:
rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra]

Result:
no goals

Proof state:
⊢ LocalizationPreserves @Finite

Tactic:
introv R hf

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
⊢ (IsLocalization.map S' f ⋯).Finite

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝³ : Algebra R S := f.toAlgebra
this✝² : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝¹ : Algebra R' S' := f'.toAlgebra
this✝ : IsScalarTower R R' S'
this : IsScalarTower R S S'
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid S M) S' := by
  rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra]

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝⁴ : Algebra R S := f.toAlgebra
this✝³ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝² : Algebra R' S' := f'.toAlgebra
this✝¹ : IsScalarTower R R' S'
this✝ : IsScalarTower R S S'
this : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
⊢ (IsLocalization.map S' f ⋯).Finite