∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S} (hf : f.EssFiniteType) {g₁ g₂ : S →+* T},
  g₁.comp f = g₂.comp f → (∀ x ∈ hf.finset, g₁ x = g₂ x) → g₁ = g₂