-- Mathlib/RingTheory/RingHom/Locally.lean
/-- In the definition of `Locally` we may replace `Localization.Away` with an arbitrary
algebra satisfying `IsLocalization.Away`. -/
lemma locally_iff_isLocalization (hP : RespectsIso P) (f : R →+* S) :
    Locally P f ↔ ∃ (s : Finset S) (_ : Ideal.span (s : Set S) = ⊤),
      ∀ t ∈ s, ∀ (Sₜ : Type u) [CommRing Sₜ] [Algebra S Sₜ] [IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)

Proof state:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ).toRingEquiv
this : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t))
⊢ P (e.toRingHom.comp ((algebraMap S (Localization.Away t)).comp f))

Tactic:
exact hP.left _ _ (hs t ht)

Result:
no goals

Proof state:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ).toRingEquiv
this : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t))
⊢ P ((algebraMap S Sₜ).comp f)

Tactic:
rw [this, RingHom.comp_assoc]

Result:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ).toRingEquiv
this : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t))
⊢ P (e.toRingHom.comp ((algebraMap S (Localization.Away t)).comp f))

Proof state:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝ :
  ∃ s,
    ∃ (_ : Ideal.span ↑s = ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
          P ((algebraMap S Sₜ).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Tactic:
exact ⟨s, hsone, fun t ht ↦ hs t ht _⟩

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) ↔
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
            P ((algebraMap S Sₜ).comp f)

Tactic:
refine ⟨fun ⟨s, hsone, hs⟩ ↦ ⟨s, hsone, fun t ht Sₜ _ _ _ ↦ ?_⟩, fun ⟨s, hsone, hs⟩ ↦ ?_⟩

Result:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
⊢ P ((algebraMap S Sₜ).comp f)

case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝ :
  ∃ s,
    ∃ (_ : Ideal.span ↑s = ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
          P ((algebraMap S Sₜ).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Proof state:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
⊢ P ((algebraMap S Sₜ).comp f)

Tactic:
let e : Localization.Away t ≃+* Sₜ :=
  (IsLocalization.algEquiv (Submonoid.powers t) _ _).toRingEquiv

Result:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ).toRingEquiv
⊢ P ((algebraMap S Sₜ).comp f)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) f ↔
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
            P ((algebraMap S Sₜ).comp f)

Tactic:
rw [locally_iff_finite P f]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) ↔
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
            P ((algebraMap S Sₜ).comp f)