-- Mathlib/RingTheory/RingHom/FinitePresentation.lean
theorem finitePresentation_holdsForLocalizationAway :
    HoldsForLocalizationAway @FinitePresentation

Proof state:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FinitePresentation R S

Tactic:
exact IsLocalization.Away.finitePresentation r

Result:
no goals

Proof state:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FinitePresentation R S
⊢ (algebraMap R S).FinitePresentation

Tactic:
rw [RingHom.FinitePresentation]

Result:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FinitePresentation R S
⊢ Algebra.FinitePresentation R S

Proof state:
⊢ HoldsForLocalizationAway @FinitePresentation

Tactic:
introv R _

Result:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap R S).FinitePresentation

Proof state:
case h.e'_5
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FinitePresentation R S
⊢ (algebraMap R S).toAlgebra = inst✝¹

Tactic:
ext

Result:
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FinitePresentation R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Proof state:
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FinitePresentation R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Tactic:
rw [Algebra.smul_def]

Result:
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FinitePresentation R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    (algebraMap R S) r✝ * x✝

Proof state:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FinitePresentation R S
⊢ Algebra.FinitePresentation R S

Tactic:
convert this

Result:
case h.e'_5
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FinitePresentation R S
⊢ (algebraMap R S).toAlgebra = inst✝¹

Proof state:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap R S).FinitePresentation

Tactic:
suffices Algebra.FinitePresentation R S by
  rw [RingHom.FinitePresentation]
  convert this; ext
  rw [Algebra.smul_def]; rfl

Result:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FinitePresentation R S

Proof state:
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FinitePresentation R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    (algebraMap R S) r✝ * x✝

Tactic:
rfl

Result:
no goals