-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) →
  CommRingCat :=
  fun (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) ↦
    of
      ↥(S.snd (β := fun (n : ℕ) ↦
              (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))).snd
          (β :=
          fun
            (R :
              Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))) →
                Subtype Q') ↦
          Subring
            ((i :
                Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))))) →
              (↑(↑(R i) : CommRingCat) : Type u))))
S : CommRingCat
hS : P S
s : Set (↑S : Type u)
hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
hs' : s.Finite
S' : (f : (↑s : Type u)) → CommRingCat
hS' : ∀ (f : (↑s : Type u)), Q' (S' f)
e : ∀ (f : (↑s : Type u)), Nonempty.{u + 1} (of (Localization.Away (↑f : (↑S : Type u))) ≅ S' f)
φ : (↑S : Type u) →+*
  (i : Fin (Nat.card.{u} (↑s : Type u))) →
    (↑(S' ((Equiv.symm (Finite.equivFin (↑s : Type u)) : (a : Fin (Nat.card (↑s : Type u))) → (↑s : Type u)) i)) :
      Type u) :=
  @RingHom.comp _ ((i : (↑s : Type u)) → (↑(of (Localization.Away (↑i : (↑S : Type u)))) : Type u)) _ _
    (Pi.nonAssocSemiring (f := fun (i : (↑s : Type u)) ↦ (↑(of (Localization.Away (↑i : (↑S : Type u)))) : Type u))) _
    (RingEquiv.toRingHom
      (RingEquiv.trans (S := (i : (↑s : Type u)) → (↑(S' i) : Type u))
        (RingEquiv.piCongrRight (R := fun (i : (↑s : Type u)) ↦
          (↑(of (Localization.Away (↑i : (↑S : Type u)))) : Type u)) (S := fun (i : (↑s : Type u)) ↦ (↑(S' i) : Type u))
          fun (i : (↑s : Type u)) ↦ ⋯.some.commRingCatIsoToRingEquiv)
        (RingEquiv.symm
          (RingEquiv.piCongrLeft (fun (x : (↑s : Type u)) ↦ (↑(S' x) : Type u))
            (Equiv.symm (Finite.equivFin (↑s : Type u)))))))
    (algebraMap (↑S : Type u) ((i : (↑s : Type u)) → (↑(of (Localization.Away (↑i : (↑S : Type u)))) : Type u)))
hφ :
  Function.Injective (α := (↑S : Type u)) (β :=
    (i : Fin (Nat.card.{u} (↑s : Type u))) →
      (↑(S' ((Equiv.symm (Finite.equivFin (↑s : Type u)) : (a : Fin (Nat.card (↑s : Type u))) → (↑s : Type u)) i)) :
        Type u))
    (⇑φ :
      (a : (↑S : Type u)) →
        (i : Fin (Nat.card (↑s : Type u))) →
          (↑(S' (((Finite.equivFin (↑s : Type u)).symm : (a : Fin (Nat.card (↑s : Type u))) → (↑s : Type u)) i)) :
            Type u))
⊢ S ≅
    f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))
        (Nat.card.{u} (↑s : Type u))
        (Sigma.mk (β := fun (R : Fin (Nat.card.{u} (↑s : Type u)) → Subtype Q') ↦
          Subring ((i : Fin (Nat.card.{u} (↑s : Type u))) → (↑(↑(R i) : CommRingCat) : Type u)))
          ((fun (f : (↑s : Type u)) ↦ Subtype.mk (p := Q') (S' f) ⋯) ∘
            (⇑(Equiv.symm (Finite.equivFin (↑s : Type u))) : (a : Fin (Nat.card (↑s : Type u))) → (↑s : Type u)))
          φ.range))

Tactic:
exact (RingEquiv.ofBijective φ.rangeRestrict
    ⟨φ.injective_codRestrict.mpr hφ, φ.rangeRestrict_surjective⟩).toCommRingCatIso

Premises used: Iff.mpr, RingHom.rangeRestrict_surjective, RingEquiv.ofBijective, RingHom.injective_codRestrict, RingEquiv.toCommRingCatIso, RingHom.rangeRestrict, And.intro