-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (hypothesis)
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)))
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have 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))
Tactic: have hφ : Function.Injective φ := by
    dsimp only [RingHom.coe_comp, φ]
    refine (RingEquiv.injective _).comp (Localization.algebraMap_injective_of_span_eq_top _ hs)