-- 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)
⊢ ∀ (i : { x // x ∈ sf } × { x // x ∈ sg }),
    P
      ((algebraMap T
            ((fun x =>
                match x with
                | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
              i)).comp
        (g.comp f))

Tactic:
intro ⟨a, b⟩

Result:
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 }
⊢ P
    ((algebraMap T
          ((fun x =>
              match x with
              | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
            (a, b))).comp
      (g.comp f))

Proof state:
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
⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => P

Tactic:
intro R S T _ _ _ f g hf hg

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
hf : Locally (fun {R S} [CommRing R] [CommRing S] => P) f
hg : Locally (fun {R S} [CommRing R] [CommRing S] => P) g
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) (g.comp f)

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
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)
x : R
⊢ (algebraMap T (Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))) (g (f x)) =
    (algebraMap (Localization.Away ↑b) (Localization.Away (g' ↑a))) (g' (f x))

Tactic:
rfl

Result:
no goals

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).comp ((algebraMap S (Localization.Away ↑a)).comp f))

Tactic:
apply hPc _ _ (hsf a.val a.property)

Result:
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)