-- Mathlib/RingTheory/LocalProperties/Basic.lean
lemma RingHom.OfLocalizationSpan.ofIsLocalization
    (hP : RingHom.OfLocalizationSpan P) (hPi : RingHom.RespectsIso P)
    {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) (hs : Ideal.span s = ⊤)
    (hT : ∀ r : s, ∃ (Rᵣ Sᵣ : Type u) (_ : CommRing Rᵣ) (_ : CommRing Sᵣ)
      (_ : Algebra R Rᵣ) (_ : Algebra S Sᵣ) (_ : IsLocalization.Away r.val Rᵣ)
      (_ : IsLocalization.Away (f r.val) Sᵣ) (fᵣ : Rᵣ →+* Sᵣ)
      (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f),
        P fᵣ) : P f

Proof state:
case h.a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
e₂ : Sᵣ ≃+* Localization (Submonoid.powers (f ↑r)) :=
  (IsLocalization.algEquiv (Submonoid.powers (f ↑r)) (Localization (Submonoid.powers (f ↑r))) Sᵣ).symm.toRingEquiv
x : R
this : fᵣ ((algebraMap R Rᵣ) x) = (algebraMap S Sᵣ) (f x)
⊢ ((Localization.awayMap f ↑r).comp (algebraMap R (Localization.Away ↑r))) x =
    (((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom).comp (algebraMap R (Localization.Away ↑r))) x

Tactic:
simp [-AlgEquiv.symm_toRingEquiv, e₂, e₁, Localization.awayMap, IsLocalization.Away.map, this]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
⊢ P (Localization.awayMap f ↑r)

Tactic:
let e₁ := (Localization.algEquiv (.powers r.val) Rᵣ).toRingEquiv

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
⊢ P (Localization.awayMap f ↑r)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
e₂ : Sᵣ ≃+* Localization (Submonoid.powers (f ↑r)) :=
  (IsLocalization.algEquiv (Submonoid.powers (f ↑r)) (Localization (Submonoid.powers (f ↑r))) Sᵣ).symm.toRingEquiv
⊢ P (Localization.awayMap f ↑r)

Tactic:
have : Localization.awayMap f r.val =
    (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom := by
  apply IsLocalization.ringHom_ext (.powers r.val)
  ext x
  have : fᵣ ((algebraMap R Rᵣ) x) = algebraMap S Sᵣ (f x) := by
    rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]
  simp [-AlgEquiv.symm_toRingEquiv, e₂, e₁, Localization.awayMap, IsLocalization.Away.map, this]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
e₂ : Sᵣ ≃+* Localization (Submonoid.powers (f ↑r)) :=
  (IsLocalization.algEquiv (Submonoid.powers (f ↑r)) (Localization (Submonoid.powers (f ↑r))) Sᵣ).symm.toRingEquiv
this : Localization.awayMap f ↑r = (e₂.toRingHom.comp fᵣ).comp e₁.toRingHom
⊢ P (Localization.awayMap f ↑r)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
⊢ ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => P) (Localization.awayMap f ↑r)

Tactic:
intro r

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
⊢ P (Localization.awayMap f ↑r)