-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` is stable under composition with localization away maps on the left,
then so is `Locally P`. -/
lemma locally_StableUnderCompositionWithLocalizationAwaySource
    (hPa : StableUnderCompositionWithLocalizationAwaySource P) :
    StableUnderCompositionWithLocalizationAwaySource (Locally P)

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

Tactic:
intro R S T _ _ _ _ r _ f ⟨s, hsone, hs⟩

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) (f.comp (algebraMap R S))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp f)
t : T
ht : t ∈ s
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (((algebraMap T (Localization.Away t)).comp f).comp (algebraMap R S))

Tactic:
exact hPa _ r _ (hs t ht)

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp f)
t : T
ht : t ∈ s
⊢ (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (f.comp (algebraMap R S)))

Tactic:
rw [← comp_assoc]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp f)
t : T
ht : t ∈ s
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (((algebraMap T (Localization.Away t)).comp f).comp (algebraMap R S))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) (f.comp (algebraMap R S))

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

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp f)
t : T
ht : t ∈ s
⊢ (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (f.comp (algebraMap R S)))