-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` respects isomorphism, so does `Locally P`. -/
lemma locally_respectsIso (hPi : RespectsIso P) : RespectsIso (Locally P) where
  left {R S T} _ _ _ f e := fun ⟨s, hsone, hs⟩ ↦ by
    refine ⟨e '' s, ?_, ?_⟩
    · rw [← Ideal.map_span, hsone, Ideal.map_top]
    · rintro - ⟨a, ha, rfl⟩
      let e' : Localization.Away a ≃+* Localization.Away (e a) :=
        IsLocalization.ringEquivOfRingEquiv _ _ e (Submonoid.map_powers e a)
      have : (algebraMap T (Localization.Away (e a))).comp e.toRingHom =
          e'.toRingHom.comp (algebraMap S (Localization.Away a))

Proof state:
case a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso 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
x✝ : (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
x : S
⊢ ((algebraMap T (Localization.Away (e a))).comp e.toRingHom) x =
    (e'.toRingHom.comp (algebraMap S (Localization.Away a))) x

Tactic:
simp [e']

Result:
no goals

Proof state:
case refine_2.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso 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
x✝ : (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
⊢ P ((algebraMap T (Localization.Away (e a))).comp (e.toRingHom.comp f))

Tactic:
let e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv _ _ e (Submonoid.map_powers e a)

Result:
case refine_2.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso 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
x✝ : (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
⊢ P ((algebraMap T (Localization.Away (e a))).comp (e.toRingHom.comp f))

Proof state:
case refine_2.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso 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
x✝ : (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
this :
  (algebraMap T (Localization.Away (e a))).comp e.toRingHom = e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P (e'.toRingHom.comp ((algebraMap S (Localization.Away a)).comp f))

Tactic:
apply hPi.left

Result:
case refine_2.intro.intro.x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso 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
x✝ : (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
this :
  (algebraMap T (Localization.Away (e a))).comp e.toRingHom = e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P ((algebraMap S (Localization.Away a)).comp f)

Proof state:
case refine_2.intro.intro.x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso 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
x✝ : (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
this :
  (algebraMap T (Localization.Away (e a))).comp e.toRingHom = e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P ((algebraMap S (Localization.Away a)).comp f)

Tactic:
exact hs a ha

Result:
no goals

Proof state:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso 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
x✝ : (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
⊢ ∀ t ∈ ⇑e '' s,
    (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (e.toRingHom.comp f))

Tactic:
rintro - ⟨a, ha, rfl⟩

Result:
case refine_2.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso 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
x✝ : (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
⊢ P ((algebraMap T (Localization.Away (e a))).comp (e.toRingHom.comp f))

Proof state:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso 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
x✝ : (fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
⊢ Ideal.span (⇑e '' s) = ⊤

Tactic:
rw [← Ideal.map_span, hsone, Ideal.map_top]

Result:
no goals