-- Mathlib/RingTheory/LocalProperties/Basic.lean
/-- Variant of `RingHom.OfLocalizationSpan.ofIsLocalization` where
`fᵣ = IsLocalization.Away.map`. -/
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ᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f r)) : P f

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,
      ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
⊢ P f

Tactic:
apply hP.ofIsLocalization hPi _ s hs

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,
      ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
⊢ ∀ (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ᵣ

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,
      ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
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ᵣ

Tactic:
obtain ⟨Rᵣ, Sᵣ, _, _, _, _, _, _, hf⟩ := hT r

Result:
case 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,
      ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
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ᵣ
hf : P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
⊢ ∃ 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ᵣ

Proof state:
case 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,
      ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
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ᵣ
hf : P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
⊢ ∃ 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ᵣ

Tactic:
exact ⟨Rᵣ, Sᵣ, inferInstance, inferInstance, inferInstance, inferInstance,
  inferInstance, inferInstance, IsLocalization.Away.map Rᵣ Sᵣ f r, IsLocalization.map_comp _, hf⟩

Result:
no goals

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,
      ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
⊢ ∀ (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ᵣ

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,
      ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
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ᵣ