-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` holds for localization away maps, then so does `Locally P`. -/
lemma locally_holdsForLocalizationAway (hPa : HoldsForLocalizationAway P) :
    HoldsForLocalizationAway (Locally P)

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ ∃ (_ : Ideal.span {1} = ⊤),
    ∀ t ∈ {1}, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp (algebraMap R S))

Tactic:
simp only [Set.mem_singleton_iff, forall_eq, Ideal.span_singleton_one, exists_const]

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P

Tactic:
introv R _

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) (algebraMap R S)

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))

Tactic:
haveI : IsLocalization.Away r (Localization.Away (1 : S)) :=
  IsLocalization.isLocalization_of_algEquiv (Submonoid.powers r) e

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away 1)
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away 1)
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))

Tactic:
rw [← IsScalarTower.algebraMap_eq]

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away 1)
⊢ P (algebraMap R (Localization.Away 1))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid S

Tactic:
simp

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) (algebraMap R S)

Tactic:
use {1}

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ ∃ (_ : Ideal.span {1} = ⊤),
    ∀ t ∈ {1}, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp (algebraMap R S))

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away 1)
⊢ P (algebraMap R (Localization.Away 1))

Tactic:
apply hPa _ r

Result:
no goals

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))

Tactic:
let e : S ≃ₐ[R] (Localization.Away (1 : S)) :=
  (IsLocalization.atUnits S (Submonoid.powers 1) (by simp)).restrictScalars R

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))