-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
intro intro₁ intro₂ intro₃ intro₄ intro₅ intro₆ intro₇ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          g →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          (g.comp f)
intro₈ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T)
    (hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        g →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦
          (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
        (g.comp f)
intro₉ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T)
    (hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f)
    (hg : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
intro₁₀ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T)
    (hf :
      ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
        ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f))
    (hg :
      ∃ (s : Finset T) (_ : Eq (α := Ideal T) (Ideal.span (↑s : Set T)) ⊤),
        ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
intro₁₁ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T)
    (hg :
      ∃ (s : Finset T) (_ : Eq (α := Ideal T) (Ideal.span (↑s : Set T)) ⊤),
        ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g))
    (sf : Finset S) (hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤)
    (hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
intro₁₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T)
    (sf : Finset S) (hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤)
    (hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) (sg : Finset T)
    (hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤)
    (hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
intro₁₃ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T)
    (sf : Finset S) (hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤)
    (hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) (sg : Finset T)
    (hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤)
    (hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)),
    ∃ (ι : Type u) (s : ι → T) (_ : Eq (α := Ideal T) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
      (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra T (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
      ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap T (Sₜ i)) (g.comp f))
refine_1 :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T)
    (sf : Finset S) (hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤)
    (hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) (sg : Finset T)
    (hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤)
    (hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)),
    Eq.{u + 1} (α := Ideal T)
      (Ideal.span
        (Set.range fun (x : ↥sf × ↥sg) ↦
          match (motive := ↥sf × ↥sg → T) x with
          | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T)))
      ⊤
refine_2 refine_2₁ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T)
    (sf : Finset S) (hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤)
    (hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)) (sg : Finset T)
    (hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤)
    (hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)) (i : ↥sf × ↥sg),
    P (S :=
      (fun (x : ↥sf × ↥sg) ↦
          (match (motive := ↥sf × ↥sg → Type u) x with
            | (a, b) =>
              Localization.Away (M := Localization.Away (↑b : T))
                ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                    ((g : (a : S) → T) (↑a : S)) :
                  Localization.Away (↑b : T)) :
            Type u))
        i)
      (comp
        (algebraMap T
          ((fun (x : ↥sf × ↥sg) ↦
              (match (motive := ↥sf × ↥sg → Type u) x with
                | (a, b) =>
                  Localization.Away (M := Localization.Away (↑b : T))
                    ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                        ((g : (a : S) → T) (↑a : S)) :
                      Localization.Away (↑b : T)) :
                Type u))
            i))
        (g.comp f))
⊢ StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P

Tactic:
classical
  intro R S T _ _ _ f g hf hg
  rw [locally_iff_finite] at hf hg
  obtain ⟨sf, hsfone, hsf⟩ := hf
  obtain ⟨sg, hsgone, hsg⟩ := hg
  rw [locally_iff_exists hPi]
  refine ⟨sf × sg, fun (a, b) ↦ g a * b, ?_,
      fun (a, b) ↦ Localization.Away ((algebraMap T (Localization.Away b.val)) (g a.val)),
      inferInstance, inferInstance, inferInstance, ?_⟩
  · rw [eq_top_iff, ← hsgone, Ideal.span_le]
    intro t ht
    have : 1 ∈ Ideal.span (Set.range <| fun a : sf ↦ a.val) := by simp [hsfone]
    simp only [Ideal.mem_span_range_iff_exists_fun, SetLike.mem_coe] at this ⊢
    obtain ⟨cf, hcf⟩ := this
    let cg : sg → T := Pi.single ⟨t, ht⟩ 1
    use fun (a, b) ↦ g (cf a) * cg b
    simp [cg, Pi.single_apply, Fintype.sum_prod_type, ← mul_assoc, ← Finset.sum_mul, ← map_mul,
      ← map_sum, hcf] at hcf ⊢
  · intro ⟨a, b⟩
    let g' := (algebraMap T (Localization.Away b.val)).comp g
    let a' := (algebraMap T (Localization.Away b.val)) (g a.val)
    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
    simp only [this, a']
    apply hPc _ _ (hsf a.val a.property)
    apply @hPl _ _ _ _ g' _ _ _ _ _ _ _ _ ?_ (hsg b.val b.property)
    exact IsLocalization.Away.instMapRingHomPowersOfCoe (Localization.Away (g' a.val)) a.val

Premises used: Ideal.span_le, eq_top_iff, Pi.single_apply, mul_assoc, map_sum, map_mul, Ideal.mem_span_range_iff_exists_fun, SetLike.mem_coe, RingHom.locally_iff_finite, RingHom.locally_iff_exists, Fintype.sum_prod_type, Finset.sum_mul