-- Mathlib/RingTheory/LocalProperties/Basic.lean
lemma RingHom.StableUnderCompositionWithLocalizationAway.respectsIso
    (hP : StableUnderCompositionWithLocalizationAway P) :
    RespectsIso P where
  left {R S T} _ _ _ f e hf

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
this : Algebra R S := e.toRingHom.toAlgebra
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

Tactic:
have : IsLocalization.Away (1 : R) S :=
  IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
this✝ : Algebra R S := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 S
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (e.toRingHom.comp f)

Tactic:
letI := e.toRingHom.toAlgebra

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
this : Algebra S T := e.toRingHom.toAlgebra
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (e.toRingHom.comp f)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

Tactic:
letI := e.toRingHom.toAlgebra

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
this : Algebra R S := e.toRingHom.toAlgebra
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
this✝ : Algebra R S := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 S
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

Tactic:
exact hP.left S (1 : R) f hf

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
this✝ : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 T
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (e.toRingHom.comp f)

Tactic:
exact hP.right T (1 : S) f hf

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
this : Algebra S T := e.toRingHom.toAlgebra
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (e.toRingHom.comp f)

Tactic:
have : IsLocalization.Away (1 : S) T :=
  IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
this✝ : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 T
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (e.toRingHom.comp f)