-- 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_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 : 1 ∈ Ideal.span (Set.range fun a => ↑a)
⊢ t ∈
    ↑(Ideal.span
        (Set.range fun x =>
          match x with
          | (a, b) => g ↑a * ↑b))

Tactic:
simp only [mem_ideal_span_range_iff_exists_fun, SetLike.mem_coe] at this ⊢

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
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

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

Tactic:
rw [locally_iff_finite] at 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 : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
hg : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap T (Localization.Away t)).comp g)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) (g.comp f)

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)
⊢ 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))

Tactic:
have : (algebraMap T <| Localization.Away a').comp (g.comp f) =
    (Localization.awayMap g' a.val).comp ((algebraMap S (Localization.Away a.val)).comp f) := by
  ext x
  simp only [coe_comp, Function.comp_apply, a']
  change _ = Localization.awayMap g' a.val (algebraMap S _ (f x))
  simp only [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_eq]
  rfl

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