-- Mathlib/RingTheory/LocalProperties/Basic.lean
lemma RingHom.LocalizationAwayPreserves.respectsIso
    (hP : LocalizationAwayPreserves 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 : LocalizationAwayPreserves 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 S R := e.symm.toRingHom.toAlgebra
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (f.comp e.toRingHom)

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

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 S R := e.symm.toRingHom.toAlgebra
this : IsLocalization.Away 1 R
⊢ (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 : LocalizationAwayPreserves 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 S R := e.symm.toRingHom.toAlgebra
this : IsLocalization.Away 1 R
⊢ IsUnit (f 1)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 S R := e.symm.toRingHom.toAlgebra
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1

Tactic:
have : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f :=
  IsLocalization.map_comp ..

Result:
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 S R := e.symm.toRingHom.toAlgebra
this✝¹ : IsLocalization.Away 1 R
this✝ : IsLocalization.Away (f 1) T
this : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 R
this : IsLocalization.Away (f 1) T
⊢ e.toRingHom.comp f = (algebraMap S T).comp f

Tactic:
rfl

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 R
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (e.toRingHom.comp f)

Tactic:
have : IsLocalization.Away (f 1) T :=
  IsLocalization.away_of_isUnit_of_bijective _ (by simp) e.bijective

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 R
this : IsLocalization.Away (f 1) T
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (e.toRingHom.comp f)

Proof state:
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 R
this : IsLocalization.Away (f 1) T
⊢ e.toRingHom.comp f = IsLocalization.Away.map R T f 1

Tactic:
trans (IsLocalization.Away.map R T f 1).comp (algebraMap R R)

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 R
this : IsLocalization.Away (f 1) T
⊢ e.toRingHom.comp f = (IsLocalization.Away.map R T f 1).comp (algebraMap R R)

P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 R
this : IsLocalization.Away (f 1) T
⊢ (IsLocalization.Away.map R T f 1).comp (algebraMap R R) = IsLocalization.Away.map R T f 1

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 : LocalizationAwayPreserves 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:
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 S R := e.symm.toRingHom.toAlgebra
this✝¹ : IsLocalization.Away 1 R
this✝ : IsLocalization.Away (f 1) T
this : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1

Tactic:
conv_lhs => rw [← this, RingHom.comp_assoc]

Result:
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves 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 S R := e.symm.toRingHom.toAlgebra
this✝¹ : IsLocalization.Away 1 R
this✝ : IsLocalization.Away (f 1) T
this : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f
⊢ (IsLocalization.Away.map R T f 1).comp (e.symm.toRingHom.comp e.toRingHom) = IsLocalization.Away.map R T f 1