-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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))
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have refine : 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) sorry) ∘
          (⇑(Equiv.symm (Finite.equivFin (↑s : Type u))) : (a : Fin (Nat.card (↑s : Type u))) → (↑s : Type u)))
        φ.range))
Tactic: refine ⟨_, ⟨Nat.card s, (fun f ↦ ⟨S' f, hS' f⟩) ∘ hs'.equivFin.symm, φ.range⟩, ⟨?_⟩⟩