∀ {α : Type u_6} {β : Type u_7} {inst : Bornology α} {inst_1 : Bornology β} {toFun : α → β}
  {comap_cobounded_le' : Filter.comap toFun (Bornology.cobounded β) ≤ Bornology.cobounded α} {toFun_1 : α → β}
  {comap_cobounded_le'_1 : Filter.comap toFun_1 (Bornology.cobounded β) ≤ Bornology.cobounded α},
  { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' } =
      { toFun := toFun_1, comap_cobounded_le' := comap_cobounded_le'_1 } →
    toFun = toFun_1