-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` preserves localizations, then `Locally P` is stable under composition if `P` is. -/
lemma locally_stableUnderComposition (hPi : RespectsIso P) (hPl : LocalizationPreserves P)
    (hPc : StableUnderComposition P) :
    StableUnderComposition (Locally P)

Proof state:
case intro.intro.intro.intro.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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : { x // x ∈ sf }
b : { x // x ∈ sg }
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
this :
  (algebraMap T (Localization.Away a')).comp (g.comp f) =
    (Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f)
⊢ P (Localization.awayMap g' ↑a)

Tactic:
apply @hPl _ _ _ _ g' _ _ _ _ _ _ _ _ ?_ (hsg b.val b.property)

Result:
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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : { x // x ∈ sf }
b : { x // x ∈ sg }
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
this :
  (algebraMap T (Localization.Away a')).comp (g.comp f) =
    (Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f)
⊢ IsLocalization (Submonoid.map g' (Submonoid.powers ↑a))
    (Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))

Proof state:
case intro.intro.intro.intro.refine_1.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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
cf : { x // x ∈ sf } → S
hcf : ∑ i : { x // x ∈ sf }, cf i * ↑i = 1
⊢ ∃ c, ∑ i : { x // x ∈ sf } × { x // x ∈ sg }, c i * (g ↑i.1 * ↑i.2) = t

Tactic:
let cg : sg → T := Pi.single ⟨t, ht⟩ 1

Result:
case intro.intro.intro.intro.refine_1.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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
cf : { x // x ∈ sf } → S
hcf : ∑ i : { x // x ∈ sf }, cf i * ↑i = 1
cg : { x // x ∈ sg } → T := Pi.single ⟨t, ht⟩ 1
⊢ ∃ c, ∑ i : { x // x ∈ sf } × { x // x ∈ sg }, c i * (g ↑i.1 * ↑i.2) = t

Proof state:
case intro.intro.intro.intro.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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
⊢ ↑sg ⊆
    ↑(Ideal.span
        (Set.range fun x =>
          match x with
          | (a, b) => g ↑a * ↑b))

Tactic:
intro t ht

Result:
case intro.intro.intro.intro.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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
⊢ t ∈
    ↑(Ideal.span
        (Set.range fun x =>
          match x with
          | (a, b) => g ↑a * ↑b))

Proof state:
case intro.intro.intro.intro.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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
this : ∃ c, ∑ i : { x // x ∈ sf }, c i * ↑i = 1
⊢ ∃ c, ∑ i : { x // x ∈ sf } × { x // x ∈ sg }, c i * (g ↑i.1 * ↑i.2) = t

Tactic:
obtain ⟨cf, hcf⟩ := this

Result:
case intro.intro.intro.intro.refine_1.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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
cf : { x // x ∈ sf } → S
hcf : ∑ i : { x // x ∈ sf }, cf i * ↑i = 1
⊢ ∃ c, ∑ i : { x // x ∈ sf } × { x // x ∈ sg }, c i * (g ↑i.1 * ↑i.2) = t